Documentation

d_K'38'__114 ∷ p → p → p → p → p → p → () Source #

d_Tree_122 ∷ p → p → p → p → p → p → p → p → p → () Source #

d_Value_124 ∷ p → p → p → p → p → () Source #

d_const_132 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → () → T_Value_40 Source #

du_const_132 ∷ T_Level_18 → () → T_Value_40 Source #

d_fromPair_140 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → T_Σ_14 → T_K'38'__58 Source #

du_fromPair_140 ∷ T_Level_18 → T_Value_40 → T_Σ_14 → T_K'38'__58 Source #

d_toPair_194 ∷ T_K'38'__58 → T_Σ_14 Source #

d_key_216 ∷ T_K'38'__58 → AgdaAny Source #

d_value_218 ∷ T_K'38'__58 → AgdaAny Source #

d_family_228 ∷ T_Value_40 → AgdaAny → () Source #

d_respects_230 ∷ T_Value_40 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Tree_266 ∷ p → p → p → p → p → p → () Source #

data T_Tree_266 Source #

d_Val_284 ∷ T_Value_40 → AgdaAny → () Source #

d_empty_286 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → T_Tree_266 Source #

du_empty_286 ∷ T_Tree_266 Source #

d_singleton_290 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → AgdaAny → AgdaAny → T_Tree_266 Source #

du_singleton_290 ∷ AgdaAny → AgdaAny → T_Tree_266 Source #

d_insert_298 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → AgdaAny → AgdaAny → T_Tree_266 → T_Tree_266 Source #

du_insert_298 ∷ T_StrictTotalOrder_1280 → T_Value_40 → AgdaAny → AgdaAny → T_Tree_266 → T_Tree_266 Source #

d_insertWith_308 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → AgdaAny → (Maybe AgdaAny → AgdaAny) → T_Tree_266 → T_Tree_266 Source #

du_insertWith_308 ∷ T_StrictTotalOrder_1280 → T_Value_40 → AgdaAny → (Maybe AgdaAny → AgdaAny) → T_Tree_266 → T_Tree_266 Source #

d_delete_316 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → AgdaAny → T_Tree_266 → T_Tree_266 Source #

du_delete_316 ∷ T_StrictTotalOrder_1280 → AgdaAny → T_Tree_266 → T_Tree_266 Source #

d_lookup_324 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → T_Tree_266 → AgdaAny → Maybe AgdaAny Source #

du_lookup_324 ∷ T_StrictTotalOrder_1280 → T_Value_40 → T_Tree_266 → AgdaAny → Maybe AgdaAny Source #

d_Val_342 ∷ T_StrictTotalOrder_1280 → T_Level_18 → T_Level_18 → T_Value_40 → T_Value_40 → AgdaAny → () Source #

d_Wal_344 ∷ T_StrictTotalOrder_1280 → T_Level_18 → T_Level_18 → T_Value_40 → T_Value_40 → AgdaAny → () Source #

d_map_346 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Level_18 → T_Value_40 → T_Value_40 → (AgdaAny → AgdaAny → AgdaAny) → T_Tree_266 → T_Tree_266 Source #

du_map_346 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_Tree_266 → T_Tree_266 Source #

d_Val_360 ∷ T_Value_40 → AgdaAny → () Source #

d_member_362 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → AgdaAny → T_Tree_266 → Bool Source #

du_member_362 ∷ T_StrictTotalOrder_1280 → T_Value_40 → AgdaAny → T_Tree_266 → Bool Source #

d_headTail_368 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → T_Tree_266 → Maybe T_Σ_14 Source #

du_headTail_368 ∷ T_StrictTotalOrder_1280 → T_Tree_266 → Maybe T_Σ_14 Source #

d_initLast_380 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → T_Tree_266 → Maybe T_Σ_14 Source #

du_initLast_380 ∷ T_StrictTotalOrder_1280 → T_Tree_266 → Maybe T_Σ_14 Source #

d_foldr_394 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Tree_266 → AgdaAny Source #

du_foldr_394 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Tree_266 → AgdaAny Source #

d_fromList_402 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → [T_K'38'__58] → T_Tree_266 Source #

du_fromList_402 ∷ T_StrictTotalOrder_1280 → T_Value_40 → [T_K'38'__58] → T_Tree_266 Source #

d_toList_404 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → T_Tree_266 → [T_K'38'__58] Source #

du_toList_404 ∷ T_Tree_266 → [T_K'38'__58] Source #

d_size_408 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → T_Tree_266 → Integer Source #

du_size_408 ∷ T_Tree_266 → Integer Source #

d_Val_424 ∷ T_StrictTotalOrder_1280 → T_Level_18 → T_Level_18 → T_Value_40 → T_Value_40 → AgdaAny → () Source #

d_Wal_426 ∷ T_StrictTotalOrder_1280 → T_Level_18 → T_Level_18 → T_Value_40 → T_Value_40 → AgdaAny → () Source #

d_unionWith_430 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Level_18 → T_Value_40 → T_Value_40 → (AgdaAny → AgdaAny → Maybe AgdaAny → AgdaAny) → T_Tree_266 → T_Tree_266 → T_Tree_266 Source #

du_unionWith_430 ∷ T_StrictTotalOrder_1280 → T_Value_40 → (AgdaAny → AgdaAny → Maybe AgdaAny → AgdaAny) → T_Tree_266 → T_Tree_266 → T_Tree_266 Source #

d_Val_450 ∷ T_Value_40 → AgdaAny → () Source #

d_union_452 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → T_Tree_266 → T_Tree_266 → T_Tree_266 Source #

du_union_452 ∷ T_StrictTotalOrder_1280 → T_Value_40 → T_Tree_266 → T_Tree_266 → T_Tree_266 Source #

d_unionsWith_456 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → (AgdaAny → AgdaAny → Maybe AgdaAny → AgdaAny) → [T_Tree_266] → T_Tree_266 Source #

du_unionsWith_456 ∷ T_StrictTotalOrder_1280 → T_Value_40 → (AgdaAny → AgdaAny → Maybe AgdaAny → AgdaAny) → [T_Tree_266] → T_Tree_266 Source #

d_unions_462 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → [T_Tree_266] → T_Tree_266 Source #

du_unions_462 ∷ T_StrictTotalOrder_1280 → T_Value_40 → [T_Tree_266] → T_Tree_266 Source #

d_Val_480 ∷ T_StrictTotalOrder_1280 → T_Level_18 → T_Level_18 → T_Level_18 → T_Value_40 → T_Value_40 → T_Value_40 → AgdaAny → () Source #

d_Wal_482 ∷ T_StrictTotalOrder_1280 → T_Level_18 → T_Level_18 → T_Level_18 → T_Value_40 → T_Value_40 → T_Value_40 → AgdaAny → () Source #

d_Xal_484 ∷ T_StrictTotalOrder_1280 → T_Level_18 → T_Level_18 → T_Level_18 → T_Value_40 → T_Value_40 → T_Value_40 → AgdaAny → () Source #

d_intersectionWith_488 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Level_18 → T_Level_18 → T_Value_40 → T_Value_40 → T_Value_40 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Tree_266 → T_Tree_266 → T_Tree_266 Source #

du_intersectionWith_488 ∷ T_StrictTotalOrder_1280 → T_Value_40 → T_Value_40 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Tree_266 → T_Tree_266 → T_Tree_266 Source #

d_cons_502 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Level_18 → T_Level_18 → T_Value_40 → T_Value_40 → T_Value_40 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Tree_266 → T_Tree_266 → AgdaAny → AgdaAny → T_Tree_266 → T_Tree_266 Source #

du_cons_502 ∷ T_StrictTotalOrder_1280 → T_Value_40 → T_Value_40 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Tree_266 → AgdaAny → AgdaAny → T_Tree_266 → T_Tree_266 Source #

d_Val_520 ∷ T_Value_40 → AgdaAny → () Source #

d_intersection_522 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → T_Tree_266 → T_Tree_266 → T_Tree_266 Source #

du_intersection_522 ∷ T_StrictTotalOrder_1280 → T_Value_40 → T_Tree_266 → T_Tree_266 → T_Tree_266 Source #

d_intersectionsWith_526 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [T_Tree_266] → T_Tree_266 Source #

du_intersectionsWith_526 ∷ T_StrictTotalOrder_1280 → T_Value_40 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [T_Tree_266] → T_Tree_266 Source #

d_intersections_536 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → [T_Tree_266] → T_Tree_266 Source #

du_intersections_536 ∷ T_StrictTotalOrder_1280 → T_Value_40 → [T_Tree_266] → T_Tree_266 Source #

d__'8712''63'__542 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → AgdaAny → T_Tree_266 → Bool Source #

du__'8712''63'__542 ∷ T_StrictTotalOrder_1280 → T_Value_40 → AgdaAny → T_Tree_266 → Bool Source #