Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Data.Tree.AVL.Indexed

Documentation

d__'60'_'60'__102 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → Maybe (Maybe AgdaAny) → AgdaAny → Maybe (Maybe AgdaAny) → () Source #

d__'60''8314'__104 ∷ p → p → p → p → p → p → () Source #

d__'8776''8729'__106 ∷ p → p → p → p → p → p → () Source #

d_Key'8314'_108 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → () Source #

d_irrefl'8314'_110 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T_Irrelevant_20 Source #

d_refl'8314'_112 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 Source #

du_refl'8314'_112 ∷ T_StrictTotalOrder_1036 → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 Source #

d_strictPartialOrder_114 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_StrictPartialOrder_556 Source #

du_strictPartialOrder_114 ∷ T_StrictTotalOrder_1036 → T_StrictPartialOrder_556 Source #

d_strictTotalOrder_116 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_StrictTotalOrder_1036 Source #

du_strictTotalOrder_116 ∷ T_StrictTotalOrder_1036 → T_StrictTotalOrder_1036 Source #

d_sym'8314'_118 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 → T__'8776''8729'__20 Source #

du_sym'8314'_118 ∷ T_StrictTotalOrder_1036 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 → T__'8776''8729'__20 Source #

d_trans'8314'_120 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #

du_trans'8314'_120 ∷ T_StrictTotalOrder_1036 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #

d_'8869''8314''60''91'_'93''60''8868''8314'_122 ∷ T_StrictTotalOrder_1036 → AgdaAny → T_Σ_14 Source #

du_'8869''8314''60''91'_'93''60''8868''8314'_122 ∷ T_Σ_14 Source #

d_'91'_'93''45'injective_138 ∷ T_StrictTotalOrder_1036 → T_Level_18 → () → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

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

d_Value_148 ∷ p → p → p → p → p → () Source #

d_const_150 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → () → T_Value_38 Source #

du_const_150 ∷ T_Level_18 → () → T_Value_38 Source #

d_fromPair_152 ∷ 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 #

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

d_key_154 ∷ T_K'38'__56 → AgdaAny Source #

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

d_value_158 ∷ T_K'38'__56 → AgdaAny Source #

d_key_162 ∷ T_K'38'__56 → AgdaAny Source #

d_value_164 ∷ T_K'38'__56 → AgdaAny Source #

d_family_168 ∷ T_Value_38 → AgdaAny → () Source #

d_respects_170 ∷ T_Value_38 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Tree_180 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_Tree_180 Source #

Constructors

C_leaf_192 T__'60''8314'__20
C_node_208 Integer Integer T_K'38'__56 T_Tree_180 T_Tree_180 T__'8764'_'8852'__30

d_ordered_224 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_180 → T__'60''8314'__20 Source #

du_ordered_224 ∷ T_StrictTotalOrder_1036 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_Tree_180 → T__'60''8314'__20 Source #

d_Val_236 ∷ T_Value_38 → AgdaAny → () Source #

d_V'8776'_238 ∷ T_Value_38 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_leaf'45'injective_248 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T__'60''8314'__20 → T__'8801'__12 → T__'8801'__12 Source #

d_node'45'injective'45'key_280 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → Integer → Integer → Integer → Integer → Integer → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_K'38'__56 → T_K'38'__56 → T_Tree_180 → T_Tree_180 → T_Tree_180 → T_Tree_180 → T__'8764'_'8852'__30 → T__'8764'_'8852'__30 → T__'8801'__12 → T__'8801'__12 Source #

d_cast'737'_290 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T__'60''8314'__20 → T_Tree_180 → T_Tree_180 Source #

du_cast'737'_290 ∷ T_StrictTotalOrder_1036 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T_Tree_180 → T_Tree_180 Source #

d_cast'691'_316 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_180 → T__'60''8314'__20 → T_Tree_180 Source #

du_cast'691'_316 ∷ T_StrictTotalOrder_1036 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_Tree_180 → T__'60''8314'__20 → T_Tree_180 Source #

d_join'737''8314'_366 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → Integer → Integer → T_K'38'__56 → T_Σ_14 → T_Tree_180 → T__'8764'_'8852'__30 → T_Σ_14 Source #

du_join'737''8314'_366 ∷ Integer → Integer → T_K'38'__56 → T_Σ_14 → T_Tree_180 → T__'8764'_'8852'__30 → T_Σ_14 Source #

d_join'691''8314'_456 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → Integer → Integer → T_K'38'__56 → T_Tree_180 → T_Σ_14 → T__'8764'_'8852'__30 → T_Σ_14 Source #

du_join'691''8314'_456 ∷ Integer → Integer → T_K'38'__56 → T_Tree_180 → T_Σ_14 → T__'8764'_'8852'__30 → T_Σ_14 Source #

d_join'737''8315'_532 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → Integer → Integer → T_K'38'__56 → T_Σ_14 → T_Tree_180 → T__'8764'_'8852'__30 → T_Σ_14 Source #

du_join'737''8315'_532 ∷ Integer → Integer → T_K'38'__56 → T_Σ_14 → T_Tree_180 → T__'8764'_'8852'__30 → T_Σ_14 Source #

d_join'691''8315'_594 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → Integer → Integer → T_K'38'__56 → T_Tree_180 → T_Σ_14 → T__'8764'_'8852'__30 → T_Σ_14 Source #

du_join'691''8315'_594 ∷ Integer → Integer → T_K'38'__56 → T_Tree_180 → T_Σ_14 → T__'8764'_'8852'__30 → T_Σ_14 Source #

d_headTail_648 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_180 → T_Σ_14 Source #

du_headTail_648 ∷ Integer → T_Tree_180 → T_Σ_14 Source #

d_initLast_698 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_180 → T_Σ_14 Source #

du_initLast_698 ∷ Integer → T_Tree_180 → T_Σ_14 Source #

d_join_754 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → Integer → Integer → T_Tree_180 → T_Tree_180 → T__'8764'_'8852'__30 → T_Σ_14 Source #

du_join_754 ∷ T_StrictTotalOrder_1036 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → Integer → Integer → T_Tree_180 → T_Tree_180 → T__'8764'_'8852'__30 → T_Σ_14 Source #

d_empty_790 ∷ T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T_Tree_180 Source #

du_empty_790 ∷ T__'60''8314'__20 → T_Tree_180 Source #

d_singleton_798 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → AgdaAny → AgdaAny → T_Σ_14 → T_Tree_180 Source #

du_singleton_798 ∷ AgdaAny → AgdaAny → T_Σ_14 → T_Tree_180 Source #

d_insertWith_818 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → AgdaAny → (Maybe AgdaAny → AgdaAny) → T_Tree_180 → T_Σ_14 → T_Σ_14 Source #

du_insertWith_818 ∷ T_StrictTotalOrder_1036 → T_Value_38 → AgdaAny → (Maybe AgdaAny → AgdaAny) → T_Tree_180 → T_Σ_14 → T_Σ_14 Source #

d_insert_920 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → AgdaAny → AgdaAny → T_Tree_180 → T_Σ_14 → T_Σ_14 Source #

du_insert_920 ∷ T_StrictTotalOrder_1036 → T_Value_38 → AgdaAny → AgdaAny → T_Tree_180 → T_Σ_14 → T_Σ_14 Source #

d_delete_936 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → AgdaAny → T_Tree_180 → T_Σ_14 → T_Σ_14 Source #

du_delete_936 ∷ T_StrictTotalOrder_1036 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → AgdaAny → T_Tree_180 → T_Σ_14 → T_Σ_14 Source #

d_lookup_1034 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_180 → AgdaAny → T_Σ_14 → Maybe AgdaAny Source #

du_lookup_1034 ∷ T_StrictTotalOrder_1036 → T_Value_38 → T_Tree_180 → AgdaAny → T_Σ_14 → Maybe AgdaAny Source #

d_foldr_1114 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → T_Level_18 → () → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Tree_180 → AgdaAny Source #

du_foldr_1114 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Tree_180 → AgdaAny Source #

d_toDiffList_1140 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_180 → [T_K'38'__56] → [T_K'38'__56] Source #

du_toDiffList_1140 ∷ T_Tree_180 → [T_K'38'__56] → [T_K'38'__56] Source #

d_toList_1154 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_180 → [T_K'38'__56] Source #

du_toList_1154 ∷ T_Tree_180 → [T_K'38'__56] Source #

d_size_1164 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_180 → Integer Source #

du_size_1164 ∷ T_Tree_180 → Integer Source #

d_Val_1178 ∷ T_StrictTotalOrder_1036 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → AgdaAny → () Source #

d_Wal_1180 ∷ T_StrictTotalOrder_1036 → T_Level_18 → T_Level_18 → T_Value_38 → T_Value_38 → AgdaAny → () Source #

d_map_1188 ∷ 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) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_180 → T_Tree_180 Source #

du_map_1188 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_Tree_180 → T_Tree_180 Source #