fact: Definition BuildFun av (env : StringMap.t DFFun -> Env av) {WrappedRepT} {n n'} {consSigs : Vector.t consSig n} {methSigs : Vector.t methSig n'} (adt : DecoratedADT (BuildADTSig consSigs methSigs)) P (DecomposeRep : WrappedRepT -> Rep adt -> _) (DecomposeRepCount : nat) codWrap domWrap wrappedRep (progsOK : forall midx, {prog : Stmt & (forall env_ext, LiftMethod (env env_ext) P (DecomposeRep wrappedRep) (codWrap midx) (domWrap midx) prog (Methods adt midx)) /\ NoUninitDec.is_no_uninited {| FuncCore.ArgVars := BuildArgNames (Datatypes.length _) DecomposeRepCount; FuncCore.RetVar := "ret"; FuncCore.Body := Compile.compile (CompileDFacade.compile prog) |} = true /\ (GoodModuleDec.is_arg_len_ok (Compile.compile (CompileDFacade.compile prog)) = true) /\ (GoodModuleDec.is_good_size (Datatypes.length (GetLocalVars.get_local_vars (Compile.compile (CompileDFacade.compile prog)) (BuildArgNames (Datatypes.length _) DecomposeRepCount) "ret") + Depth.depth (Compile.compile (CompileDFacade.compile prog))) = true) /\ is_disjoint (assigned prog) (StringSetFacts.of_list (BuildArgNames (Datatypes.length _) DecomposeRepCount)) = true /\ is_syntax_ok prog = true} ) : StringMap.t DFFun := List.fold_left (fun acc el => StringMap.add (methID (Vector.nth methSigs el)) (BuildDFFun env DecomposeRep _ wrappedRep (progsOK el) ) acc) (BuildFinUpTo n') (StringMap.empty _).
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.ADT.Core Bedrock.Platform.Facade.DFModule Fiat.ADTNotation Bedrock.Platform.Facade.CompileUnit2 Fiat.Common.i3list Fiat.Common.ilist3 CertifiedExtraction.Core CertifiedExtraction.FacadeUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.Extraction