Documentation

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

d_Tree_98 ∷ p → p → p → p → p → p → p → p → p → () Source #

d_Value_100 ∷ p → p → p → p → p → () Source #

d_const_106 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → () → T_Value_38 Source #

du_const_106 ∷ T_Level_18 → () → T_Value_38 Source #

d_fromPair_114 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → T_Σ_14 → T_K'38'__56 Source #

du_fromPair_114 ∷ T_Level_18 → T_Value_38 → T_Σ_14 → T_K'38'__56 Source #

d_toPair_168 ∷ T_K'38'__56 → T_Σ_14 Source #

d_key_190 ∷ T_K'38'__56 → AgdaAny Source #

d_value_192 ∷ T_K'38'__56 → AgdaAny Source #

d_family_202 ∷ T_Value_38 → AgdaAny → () Source #

d_respects_204 ∷ T_Value_38 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Tree_240 ∷ p → p → p → p → p → p → () Source #

data T_Tree_240 Source #

d_Val_258 ∷ T_Value_38 → AgdaAny → () Source #

d_empty_260 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → T_Tree_240 Source #

du_empty_260 ∷ T_Tree_240 Source #

d_singleton_264 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → AgdaAny → AgdaAny → T_Tree_240 Source #

du_singleton_264 ∷ AgdaAny → AgdaAny → T_Tree_240 Source #

d_insert_272 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → AgdaAny → AgdaAny → T_Tree_240 → T_Tree_240 Source #

du_insert_272 ∷ T_StrictTotalOrder_864 → T_Value_38 → AgdaAny → AgdaAny → T_Tree_240 → T_Tree_240 Source #

d_insertWith_282 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → AgdaAny → (Maybe AgdaAny → AgdaAny) → T_Tree_240 → T_Tree_240 Source #

du_insertWith_282 ∷ T_StrictTotalOrder_864 → T_Value_38 → AgdaAny → (Maybe AgdaAny → AgdaAny) → T_Tree_240 → T_Tree_240 Source #

d_delete_290 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → AgdaAny → T_Tree_240 → T_Tree_240 Source #

du_delete_290 ∷ T_StrictTotalOrder_864 → AgdaAny → T_Tree_240 → T_Tree_240 Source #

d_lookup_298 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → AgdaAny → T_Tree_240 → Maybe AgdaAny Source #

du_lookup_298 ∷ T_StrictTotalOrder_864 → T_Value_38 → AgdaAny → T_Tree_240 → Maybe AgdaAny Source #

d_Val_316 ∷ T_StrictTotalOrder_864 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → AgdaAny → () Source #

d_Wal_318 ∷ T_StrictTotalOrder_864 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → AgdaAny → () Source #

d_map_320 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → (AgdaAny → AgdaAny → AgdaAny) → T_Tree_240 → T_Tree_240 Source #

du_map_320 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_Tree_240 → T_Tree_240 Source #

d_Val_334 ∷ T_Value_38 → AgdaAny → () Source #

d__'8712''63'__336 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → AgdaAny → T_Tree_240 → Bool Source #

du__'8712''63'__336 ∷ T_StrictTotalOrder_864 → T_Value_38 → AgdaAny → T_Tree_240 → Bool Source #

d_headTail_342 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → T_Tree_240 → Maybe T_Σ_14 Source #

du_headTail_342 ∷ T_StrictTotalOrder_864 → T_Tree_240 → Maybe T_Σ_14 Source #

d_initLast_356 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → T_Tree_240 → Maybe T_Σ_14 Source #

du_initLast_356 ∷ T_StrictTotalOrder_864 → T_Tree_240 → Maybe T_Σ_14 Source #

d_foldr_372 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Tree_240 → AgdaAny Source #

du_foldr_372 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Tree_240 → AgdaAny Source #

d_fromList_380 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → [T_K'38'__56] → T_Tree_240 Source #

du_fromList_380 ∷ T_StrictTotalOrder_864 → T_Value_38 → [T_K'38'__56] → T_Tree_240 Source #

d_toList_382 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → T_Tree_240 → [T_K'38'__56] Source #

du_toList_382 ∷ T_Tree_240 → [T_K'38'__56] Source #

d_size_386 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → T_Tree_240 → Integer Source #

du_size_386 ∷ T_Tree_240 → Integer Source #

d_Val_402 ∷ T_StrictTotalOrder_864 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → AgdaAny → () Source #

d_Wal_404 ∷ T_StrictTotalOrder_864 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → AgdaAny → () Source #

d_unionWith_408 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → (AgdaAny → AgdaAny → Maybe AgdaAny → AgdaAny) → T_Tree_240 → T_Tree_240 → T_Tree_240 Source #

du_unionWith_408 ∷ T_StrictTotalOrder_864 → T_Value_38 → (AgdaAny → AgdaAny → Maybe AgdaAny → AgdaAny) → T_Tree_240 → T_Tree_240 → T_Tree_240 Source #

d_Val_428 ∷ T_Value_38 → AgdaAny → () Source #

d_union_430 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → T_Tree_240 → T_Tree_240 → T_Tree_240 Source #

du_union_430 ∷ T_StrictTotalOrder_864 → T_Value_38 → T_Tree_240 → T_Tree_240 → T_Tree_240 Source #

d_unionsWith_434 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → (AgdaAny → AgdaAny → Maybe AgdaAny → AgdaAny) → [T_Tree_240] → T_Tree_240 Source #

du_unionsWith_434 ∷ T_StrictTotalOrder_864 → T_Value_38 → (AgdaAny → AgdaAny → Maybe AgdaAny → AgdaAny) → [T_Tree_240] → T_Tree_240 Source #

d_unions_440 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → [T_Tree_240] → T_Tree_240 Source #

du_unions_440 ∷ T_StrictTotalOrder_864 → T_Value_38 → [T_Tree_240] → T_Tree_240 Source #

d_Val_458 ∷ T_StrictTotalOrder_864 → T_Level_18 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → T_Value_38 → AgdaAny → () Source #

d_Wal_460 ∷ T_StrictTotalOrder_864 → T_Level_18 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → T_Value_38 → AgdaAny → () Source #

d_Xal_462 ∷ T_StrictTotalOrder_864 → T_Level_18 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → T_Value_38 → AgdaAny → () Source #

d_intersectionWith_466 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → T_Value_38 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Tree_240 → T_Tree_240 → T_Tree_240 Source #

du_intersectionWith_466 ∷ T_StrictTotalOrder_864 → T_Value_38 → T_Value_38 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Tree_240 → T_Tree_240 → T_Tree_240 Source #

d_cons_480 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → T_Value_38 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Tree_240 → T_Tree_240 → AgdaAny → AgdaAny → T_Tree_240 → T_Tree_240 Source #

du_cons_480 ∷ T_StrictTotalOrder_864 → T_Value_38 → T_Value_38 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Tree_240 → AgdaAny → AgdaAny → T_Tree_240 → T_Tree_240 Source #

d_Val_498 ∷ T_Value_38 → AgdaAny → () Source #

d_intersection_500 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → T_Tree_240 → T_Tree_240 → T_Tree_240 Source #

du_intersection_500 ∷ T_StrictTotalOrder_864 → T_Value_38 → T_Tree_240 → T_Tree_240 → T_Tree_240 Source #

d_intersectionsWith_504 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [T_Tree_240] → T_Tree_240 Source #

du_intersectionsWith_504 ∷ T_StrictTotalOrder_864 → T_Value_38 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [T_Tree_240] → T_Tree_240 Source #

d_intersections_514 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → [T_Tree_240] → T_Tree_240 Source #

du_intersections_514 ∷ T_StrictTotalOrder_864 → T_Value_38 → [T_Tree_240] → T_Tree_240 Source #