Documentation

d__'8712''63'__4 ∷ T_Level_18 → () → T_String_6 → T_Tree_266 → Bool Source #

d_Map_6 ∷ T_Level_18 → () → () Source #

d_delete_8 ∷ T_Level_18 → () → T_String_6 → T_Tree_266 → T_Tree_266 Source #

d_empty_10 ∷ T_Level_18 → () → T_Tree_266 Source #

d_foldr_12 ∷ T_Level_18 → () → T_Level_18 → () → (T_String_6 → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Tree_266 → AgdaAny Source #

d_fromList_14 ∷ T_Level_18 → () → [T_Σ_14] → T_Tree_266 Source #

d_headTail_16 ∷ T_Level_18 → () → T_Tree_266 → Maybe T_Σ_14 Source #

d_initLast_18 ∷ T_Level_18 → () → T_Tree_266 → Maybe T_Σ_14 Source #

d_insert_20 ∷ T_Level_18 → () → T_String_6 → AgdaAny → T_Tree_266 → T_Tree_266 Source #

d_insertWith_22 ∷ T_Level_18 → () → T_String_6 → (Maybe AgdaAny → AgdaAny) → T_Tree_266 → T_Tree_266 Source #

d_intersection_24 ∷ T_Level_18 → () → T_Tree_266 → T_Tree_266 → T_Tree_266 Source #

d_intersectionWith_26 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → T_Tree_266 → T_Tree_266 → T_Tree_266 Source #

d_intersections_28 ∷ T_Level_18 → () → [T_Tree_266] → T_Tree_266 Source #

d_intersectionsWith_30 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → [T_Tree_266] → T_Tree_266 Source #

d_lookup_32 ∷ T_Level_18 → () → T_Tree_266 → T_String_6 → Maybe AgdaAny Source #

d_map_34 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Tree_266 → T_Tree_266 Source #

d_member_36 ∷ T_Level_18 → () → T_String_6 → T_Tree_266 → Bool Source #

d_singleton_38 ∷ T_Level_18 → () → T_String_6 → AgdaAny → T_Tree_266 Source #

d_size_40 ∷ T_Level_18 → () → T_Tree_266 → Integer Source #

d_toList_42 ∷ T_Level_18 → () → T_Tree_266 → [T_Σ_14] Source #

d_union_44 ∷ T_Level_18 → () → T_Tree_266 → T_Tree_266 → T_Tree_266 Source #

d_unionWith_46 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → Maybe AgdaAny → AgdaAny) → T_Tree_266 → T_Tree_266 → T_Tree_266 Source #

d_unions_48 ∷ T_Level_18 → () → [T_Tree_266] → T_Tree_266 Source #

d_unionsWith_50 ∷ T_Level_18 → () → (AgdaAny → Maybe AgdaAny → AgdaAny) → [T_Tree_266] → T_Tree_266 Source #

d_ExBudget_52 ∷ () Source #

data T_ExBudget_52 Source #

d_ExCPU_58 ∷ T_ExBudget_52 → Integer Source #

d_ExMem_60 ∷ T_ExBudget_52 → Integer Source #

d_fromHExBudget_64 ∷ T_HExBudget_6 → T_ExBudget_52 Source #

d_ε'8364'_68 ∷ T_ExBudget_52 Source #

d__'8729''8364'__70 ∷ T_ExBudget_52 → T_ExBudget_52 → T_ExBudget_52 Source #

d_isMonoidExBudget_80 ∷ T_IsMonoid_712 Source #

d_measures_96 ∷ T_Builtin_2 → T_Vec_28 Source #

d_builtinCost_100 ∷ T_Builtin_2 → T_BuiltinModel_68 → T_Vec_28 → T_ExBudget_52 Source #

d_argSizes_112 ∷ T_Builtin_2 → T_BuiltinModel_68 → T_Vec_28 → T_Vec_28 Source #

du_argSizes_112 ∷ T_Builtin_2 → T_Vec_28 → T_Vec_28 Source #

d_CostModel_114 ∷ () Source #

d_cekMachineCostFunction_116 ∷ T_HCekMachineCosts_4 → T_StepKind_6 → T_ExBudget_52 Source #

d_exBudgetCategoryCost_136 ∷ T__'215'__436 T_HCekMachineCosts_4 (T_Builtin_2 → T_BuiltinModel_68) → T_ExBudgetCategory_34 → T_ExBudget_52 Source #

d_machineParameters_150 ∷ T__'215'__436 T_HCekMachineCosts_4 (T_Builtin_2 → T_BuiltinModel_68) → T_MachineParameters_46 Source #

d_countingReport_154 ∷ T_ExBudget_52 → T_String_6 Source #

d_mkKeyFromExBudgetCategory_160 ∷ T_ExBudgetCategory_34 → T_String_6 Source #

d_TallyingBudget_166 ∷ () Source #

d_lookup_168 ∷ T_Tree_266 → T_ExBudgetCategory_34 → T_ExBudget_52 Source #

d_εT_188 ∷ T__'215'__436 T_Tree_266 T_ExBudget_52 Source #

d__'8729'T__190 ∷ T__'215'__436 T_Tree_266 T_ExBudget_52 → T__'215'__436 T_Tree_266 T_ExBudget_52 → T__'215'__436 T_Tree_266 T_ExBudget_52 Source #

d_u_204 ∷ T_Tree_266 → T_ExBudget_52 → T_Tree_266 → T_ExBudget_52 → T_ExBudget_52 → Maybe T_ExBudget_52 → T_ExBudget_52 Source #

du_u_204 ∷ T_ExBudget_52 → Maybe T_ExBudget_52 → T_ExBudget_52 Source #

d_TallyingBudget'45'assoc_212 ∷ a Source #

d_Tallying'45'budget'45'identity'691'_214 ∷ a Source #

d_isMonoidTallyingBudget_216 ∷ T_IsMonoid_712 Source #

d_tallyingCekMachineCost_222 ∷ T__'215'__436 T_HCekMachineCosts_4 (T_Builtin_2 → T_BuiltinModel_68) → T_ExBudgetCategory_34 → T__'215'__436 T_Tree_266 T_ExBudget_52 Source #

d_tallyingMachineParameters_230 ∷ T__'215'__436 T_HCekMachineCosts_4 (T_Builtin_2 → T_BuiltinModel_68) → T_MachineParameters_46 Source #

d_tallyingReport_234 ∷ T__'215'__436 T_Tree_266 T_ExBudget_52 → T_String_6 Source #

d_totalComputeCost_244 ∷ T_Tree_266 → T_ExBudget_52 → T_ExBudget_52 Source #

du_totalComputeCost_244 ∷ T_Tree_266 → T_ExBudget_52 Source #

d_totalBuiltinCosts_246 ∷ T_Tree_266 → T_ExBudget_52 → T_ExBudget_52 Source #

du_totalBuiltinCosts_246 ∷ T_Tree_266 → T_ExBudget_52 Source #

d_getCPU_254 ∷ T_Tree_266 → T_ExBudget_52 → T_ExBudget_52 → T_Float_6 Source #

du_getCPU_254 ∷ T_ExBudget_52 → T_Float_6 Source #

d_budgetToString_258 ∷ T_Tree_266 → T_ExBudget_52 → T_ExBudget_52 → T_String_6 Source #

du_budgetToString_258 ∷ T_ExBudget_52 → T_String_6 Source #

d_printStepCost_264 ∷ T_Tree_266 → T_ExBudget_52 → T_StepKind_6 → T_ExBudget_52 → T_String_6 Source #

du_printStepCost_264 ∷ T_StepKind_6 → T_ExBudget_52 → T_String_6 Source #

d_printStepReport_270 ∷ T_Tree_266 → T_ExBudget_52 → T_Tree_266 → T_String_6 Source #

du_printStepReport_270 ∷ T_Tree_266 → T_String_6 Source #

d_printBuiltinCost_278 ∷ T_Tree_266 → T_ExBudget_52 → T_Builtin_2 → T_ExBudget_52 → T_String_6 Source #

du_printBuiltinCost_278 ∷ T_Builtin_2 → T_ExBudget_52 → T_String_6 Source #

d_printBuiltinReport_286 ∷ T_Tree_266 → T_ExBudget_52 → T_Tree_266 → T_String_6 Source #

du_printBuiltinReport_286 ∷ T_Tree_266 → T_String_6 Source #

d_formatTimePicoseconds_294 ∷ T_Tree_266 → T_ExBudget_52 → T_Float_6 → T_String_6 Source #

du_formatTimePicoseconds_294 ∷ T_Float_6 → T_String_6 Source #