| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.Tree.AVL
Documentation
d_K'38'__106 ∷ p → p → p → p → p → p → () Source #
d_Tree_112 ∷ p → p → p → p → p → p → p → p → p → () Source #
d_Value_114 ∷ p → p → p → p → p → () Source #
d_const_120 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → () → T_Value_38 Source #
du_const_120 ∷ T_Level_18 → () → T_Value_38 Source #
d_fromPair_128 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → T_Σ_14 → T_K'38'__56 Source #
d_family_216 ∷ T_Value_38 → AgdaAny → () Source #
d_respects_218 ∷ T_Value_38 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_Tree_254 ∷ p → p → p → p → p → p → () Source #
data T_Tree_254 Source #
Constructors
| C_tree_262 Integer T_Tree_180 |
d_Val_272 ∷ T_Value_38 → AgdaAny → () Source #
d_empty_274 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → T_Tree_254 Source #
d_singleton_278 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → AgdaAny → AgdaAny → T_Tree_254 Source #
d_insert_286 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → AgdaAny → AgdaAny → T_Tree_254 → T_Tree_254 Source #
du_insert_286 ∷ T_StrictTotalOrder_1036 → T_Value_38 → AgdaAny → AgdaAny → T_Tree_254 → T_Tree_254 Source #
d_insertWith_296 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → AgdaAny → (Maybe AgdaAny → AgdaAny) → T_Tree_254 → T_Tree_254 Source #
du_insertWith_296 ∷ T_StrictTotalOrder_1036 → T_Value_38 → AgdaAny → (Maybe AgdaAny → AgdaAny) → T_Tree_254 → T_Tree_254 Source #
d_delete_304 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → AgdaAny → T_Tree_254 → T_Tree_254 Source #
d_lookup_312 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → T_Tree_254 → AgdaAny → Maybe AgdaAny Source #
du_lookup_312 ∷ T_StrictTotalOrder_1036 → T_Value_38 → T_Tree_254 → AgdaAny → Maybe AgdaAny Source #
d_Val_330 ∷ T_StrictTotalOrder_1036 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → AgdaAny → () Source #
d_Wal_332 ∷ T_StrictTotalOrder_1036 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → AgdaAny → () Source #
d_map_334 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → (AgdaAny → AgdaAny → AgdaAny) → T_Tree_254 → T_Tree_254 Source #
du_map_334 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_Tree_254 → T_Tree_254 Source #
d_Val_348 ∷ T_Value_38 → AgdaAny → () Source #
d_member_350 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → AgdaAny → T_Tree_254 → Bool Source #
d_headTail_356 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → T_Tree_254 → Maybe T_Σ_14 Source #
d_initLast_368 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → T_Tree_254 → Maybe T_Σ_14 Source #
d_foldr_382 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Tree_254 → AgdaAny Source #
du_foldr_382 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Tree_254 → AgdaAny Source #
d_fromList_390 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → [T_K'38'__56] → T_Tree_254 Source #
d_toList_392 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → T_Tree_254 → [T_K'38'__56] Source #
d_size_396 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → T_Tree_254 → Integer Source #
d_Val_412 ∷ T_StrictTotalOrder_1036 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → AgdaAny → () Source #
d_Wal_414 ∷ T_StrictTotalOrder_1036 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → AgdaAny → () Source #
d_unionWith_418 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → (AgdaAny → AgdaAny → Maybe AgdaAny → AgdaAny) → T_Tree_254 → T_Tree_254 → T_Tree_254 Source #
du_unionWith_418 ∷ T_StrictTotalOrder_1036 → T_Value_38 → (AgdaAny → AgdaAny → Maybe AgdaAny → AgdaAny) → T_Tree_254 → T_Tree_254 → T_Tree_254 Source #
d_Val_438 ∷ T_Value_38 → AgdaAny → () Source #
d_union_440 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → T_Tree_254 → T_Tree_254 → T_Tree_254 Source #
d_unionsWith_444 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → (AgdaAny → AgdaAny → Maybe AgdaAny → AgdaAny) → [T_Tree_254] → T_Tree_254 Source #
du_unionsWith_444 ∷ T_StrictTotalOrder_1036 → T_Value_38 → (AgdaAny → AgdaAny → Maybe AgdaAny → AgdaAny) → [T_Tree_254] → T_Tree_254 Source #
d_unions_450 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → [T_Tree_254] → T_Tree_254 Source #
d_Val_468 ∷ T_StrictTotalOrder_1036 → T_Level_18 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → T_Value_38 → AgdaAny → () Source #
d_Wal_470 ∷ T_StrictTotalOrder_1036 → T_Level_18 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → T_Value_38 → AgdaAny → () Source #
d_Xal_472 ∷ T_StrictTotalOrder_1036 → T_Level_18 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → T_Value_38 → AgdaAny → () Source #
d_intersectionWith_476 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → T_Value_38 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Tree_254 → T_Tree_254 → T_Tree_254 Source #
du_intersectionWith_476 ∷ T_StrictTotalOrder_1036 → T_Value_38 → T_Value_38 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Tree_254 → T_Tree_254 → T_Tree_254 Source #
d_cons_490 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → T_Value_38 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Tree_254 → T_Tree_254 → AgdaAny → AgdaAny → T_Tree_254 → T_Tree_254 Source #
du_cons_490 ∷ T_StrictTotalOrder_1036 → T_Value_38 → T_Value_38 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Tree_254 → AgdaAny → AgdaAny → T_Tree_254 → T_Tree_254 Source #
d_Val_508 ∷ T_Value_38 → AgdaAny → () Source #
d_intersection_510 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → T_Tree_254 → T_Tree_254 → T_Tree_254 Source #
du_intersection_510 ∷ T_StrictTotalOrder_1036 → T_Value_38 → T_Tree_254 → T_Tree_254 → T_Tree_254 Source #
d_intersectionsWith_514 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [T_Tree_254] → T_Tree_254 Source #
du_intersectionsWith_514 ∷ T_StrictTotalOrder_1036 → T_Value_38 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [T_Tree_254] → T_Tree_254 Source #
d_intersections_524 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → [T_Tree_254] → T_Tree_254 Source #