proposition: Lemma CompileWordListDelete: forall {A} {Wrp: FacadeWrapper W A} (vtmp vlst : StringMap.key) (env : GLabelMap.t (FuncSpec QsADTs.ADTValue)) (tenv: Telescope QsADTs.ADTValue) ext (fpointer : GLabelMap.key), vlst <> vtmp -> vtmp ∉ ext -> vlst ∉ ext -> Lifted_MapsTo ext tenv vlst (wrap (@nil A)) -> Lifted_not_mapsto_adt ext tenv vtmp -> GLabelMap.MapsTo fpointer (Axiomatic WordListADTSpec.Delete) env -> {{ tenv }} Call vtmp fpointer (vlst :: nil) {{ [[`vtmp ->> (Word.natToWord 32 0) as _]] :: (DropName vtmp (DropName vlst tenv)) }} ∪ {{ ext }} // env.
proof: Proof. repeat (SameValues_Facade_t_step || facade_cleanup_call || LiftPropertyToTelescope_t || PreconditionSet_t); facade_eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.CertifiedExtraction.Extraction.Extraction Fiat.CertifiedExtraction.Extraction.BinEncoders.Basics Fiat.CertifiedExtraction.Extraction.BinEncoders.Wrappers Fiat.CertifiedExtraction.Extraction.BinEncoders.Properties Coq.Program.Program Coq.Lists.List Bedrock.Platform.Facade.examples.QsADTs