proposition: Lemma CompileWordListPop : forall {A} {Wrp: FacadeWrapper W A}, let Wrapper := WrapSCAList : FacadeWrapper (Value ADTValue) (list A) in forall vret vlst fpointer (env: Env ADTValue) ext tenv h (t: list A), GLabelMap.find fpointer env = Some (Axiomatic WordListADTSpec.Pop) -> Lifted_MapsTo ext tenv vlst (wrap (h :: t)) -> Lifted_not_mapsto_adt ext tenv vret -> vret <> vlst -> vlst ∉ ext -> vret ∉ ext -> {{ tenv }} Call vret fpointer (vlst :: nil) {{ [[ `vret ->> h as _ ]] :: [[ `vlst ->> t as _ ]] :: DropName vlst (DropName vret tenv) }} ∪ {{ ext }} // env.
proof: Proof. repeat (SameValues_Facade_t_step || facade_cleanup_call || LiftPropertyToTelescope_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