proposition: Lemma CompileCallListBoundedNatLength: forall (vlst varg : string) (tenv : Telescope ADTValue) (ext : StringMap.t (Value ADTValue)) env (lst : BoundedList (BoundedNat 8) (pow2 8)) fLength tenv', PreconditionSet tenv' ext [[[vlst;varg]]] -> GLabelMap.MapsTo fLength (Axiomatic WordListADTSpec.Length) env -> TelEq ext tenv ([[`vlst ->> lst as _]]::tenv') -> {{ tenv }} Call varg fLength [vlst] {{ [[ ` varg ->> BoundedListLength lst as _]]::tenv }} ∪ {{ ext }} // env.
proof: Proof. intros. eapply CompileCallListSCALength; eauto. eexists; split. - reflexivity. - setoid_rewrite map_length; reflexivity. 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