proposition: Lemma CompileDelete {idx}: forall (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 (RealElemType idx))) -> Lifted_not_mapsto_adt ext tenv vtmp -> GLabelMap.MapsTo fpointer (Axiomatic 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 || injections); facade_eauto. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.CallRules.Core CertifiedExtraction.Extraction.External.Loops CertifiedExtraction.Extraction.External.FacadeLoops CertifiedExtraction.Extraction.External.Lists