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_builtinCost_96 ∷ T_Builtin_2 → T_BuiltinModel_66 → T_Vec_28 → T_ExBudget_52 Source #

d_CostModel_104 ∷ () Source #

d_cekMachineCostFunction_106 ∷ T_HCekMachineCosts_4 → T_StepKind_6 → T_ExBudget_52 Source #

d_exBudgetCategoryCost_126 ∷ T__'215'__428 T_HCekMachineCosts_4 (T_Builtin_2 → T_BuiltinModel_66) → T_ExBudgetCategory_34 → T_ExBudget_52 Source #

d_machineParameters_140 ∷ T__'215'__428 T_HCekMachineCosts_4 (T_Builtin_2 → T_BuiltinModel_66) → T_MachineParameters_46 Source #

d_countingReport_144 ∷ T_ExBudget_52 → T_String_6 Source #

d_mkKeyFromExBudgetCategory_150 ∷ T_ExBudgetCategory_34 → T_String_6 Source #

d_TallyingBudget_156 ∷ () Source #

d_lookup_158 ∷ T_Tree_266 → T_ExBudgetCategory_34 → T_ExBudget_52 Source #

d_εT_178 ∷ T__'215'__428 T_Tree_266 T_ExBudget_52 Source #

d__'8729'T__180 ∷ T__'215'__428 T_Tree_266 T_ExBudget_52 → T__'215'__428 T_Tree_266 T_ExBudget_52 → T__'215'__428 T_Tree_266 T_ExBudget_52 Source #

d_u_194 ∷ 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_194 ∷ T_ExBudget_52 → Maybe T_ExBudget_52 → T_ExBudget_52 Source #

d_TallyingBudget'45'assoc_202 ∷ a Source #

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

d_isMonoidTallyingBudget_206 ∷ T_IsMonoid_712 Source #

d_tallyingCekMachineCost_212 ∷ T__'215'__428 T_HCekMachineCosts_4 (T_Builtin_2 → T_BuiltinModel_66) → T_ExBudgetCategory_34 → T__'215'__428 T_Tree_266 T_ExBudget_52 Source #

d_tallyingMachineParameters_220 ∷ T__'215'__428 T_HCekMachineCosts_4 (T_Builtin_2 → T_BuiltinModel_66) → T_MachineParameters_46 Source #

d_tallyingReport_224 ∷ T__'215'__428 T_Tree_266 T_ExBudget_52 → T_String_6 Source #

d_totalComputeCost_234 ∷ T_Tree_266 → T_ExBudget_52 → T_ExBudget_52 Source #

du_totalComputeCost_234 ∷ T_Tree_266 → T_ExBudget_52 Source #

d_totalBuiltinCosts_236 ∷ T_Tree_266 → T_ExBudget_52 → T_ExBudget_52 Source #

du_totalBuiltinCosts_236 ∷ T_Tree_266 → T_ExBudget_52 Source #

d_getCPU_244 ∷ T_Tree_266 → T_ExBudget_52 → T_ExBudget_52 → T_Float_6 Source #

du_getCPU_244 ∷ T_ExBudget_52 → T_Float_6 Source #

d_budgetToString_248 ∷ T_Tree_266 → T_ExBudget_52 → T_ExBudget_52 → T_String_6 Source #

du_budgetToString_248 ∷ T_ExBudget_52 → T_String_6 Source #

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

du_printStepCost_254 ∷ T_StepKind_6 → T_ExBudget_52 → T_String_6 Source #

d_printStepReport_260 ∷ T_Tree_266 → T_ExBudget_52 → T_Tree_266 → T_String_6 Source #

du_printStepReport_260 ∷ T_Tree_266 → T_String_6 Source #

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

du_printBuiltinCost_268 ∷ T_Builtin_2 → T_ExBudget_52 → T_String_6 Source #

d_printBuiltinReport_276 ∷ T_Tree_266 → T_ExBudget_52 → T_Tree_266 → T_String_6 Source #

du_printBuiltinReport_276 ∷ T_Tree_266 → T_String_6 Source #

d_formatTimePicoseconds_284 ∷ T_Tree_266 → T_ExBudget_52 → T_Float_6 → T_String_6 Source #

du_formatTimePicoseconds_284 ∷ T_Float_6 → T_String_6 Source #