Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Data.Tree.AVL.Indexed

Documentation

d__'60'_'60'__88 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → Maybe (Maybe AgdaAny) → AgdaAny → Maybe (Maybe AgdaAny) → () Source #

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

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

d_Key'8314'_94 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → () Source #

d_irrefl'8314'_96 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T_'8869'_4 Source #

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

du_refl'8314'_98 ∷ T_StrictTotalOrder_864 → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 Source #

d_strictPartialOrder_100 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_StrictPartialOrder_472 Source #

du_strictPartialOrder_100 ∷ T_StrictTotalOrder_864 → T_StrictPartialOrder_472 Source #

d_strictTotalOrder_102 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_StrictTotalOrder_864 Source #

du_strictTotalOrder_102 ∷ T_StrictTotalOrder_864 → T_StrictTotalOrder_864 Source #

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

du_sym'8314'_104 ∷ T_StrictTotalOrder_864 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 → T__'8776''8729'__20 Source #

d_trans'8314'_106 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → 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'_106 ∷ T_StrictTotalOrder_864 → 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'_108 ∷ T_StrictTotalOrder_864 → AgdaAny → T_Σ_14 Source #

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

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

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

d_Value_134 ∷ p → p → p → p → p → () Source #

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

du_const_136 ∷ T_Level_18 → () → T_Value_38 Source #

d_fromPair_138 ∷ 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_138 ∷ T_Level_18 → T_Value_38 → T_Σ_14 → T_K'38'__56 Source #

d_key_140 ∷ T_K'38'__56 → AgdaAny Source #

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

d_value_144 ∷ T_K'38'__56 → AgdaAny Source #

d_key_148 ∷ T_K'38'__56 → AgdaAny Source #

d_value_150 ∷ T_K'38'__56 → AgdaAny Source #

d_family_154 ∷ T_Value_38 → AgdaAny → () Source #

d_respects_156 ∷ T_Value_38 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Tree_166 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_Tree_166 Source #

Constructors

C_leaf_178 T__'60''8314'__20
C_node_194 Integer Integer T_K'38'__56 T_Tree_166 T_Tree_166 T__'8764'_'8852'__30

d_ordered_210 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_166 → T__'60''8314'__20 Source #

du_ordered_210 ∷ T_StrictTotalOrder_864 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_Tree_166 → T__'60''8314'__20 Source #

d_Val_222 ∷ T_Value_38 → AgdaAny → () Source #

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

d_leaf'45'injective_234 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → 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_266 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → 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_166 → T_Tree_166 → T_Tree_166 → T_Tree_166 → T__'8764'_'8852'__30 → T__'8764'_'8852'__30 → T__'8801'__12 → T__'8801'__12 Source #

d_cast'737'_276 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T__'60''8314'__20 → T_Tree_166 → T_Tree_166 Source #

du_cast'737'_276 ∷ T_StrictTotalOrder_864 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T_Tree_166 → T_Tree_166 Source #

d_cast'691'_302 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_166 → T__'60''8314'__20 → T_Tree_166 Source #

du_cast'691'_302 ∷ T_StrictTotalOrder_864 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_Tree_166 → T__'60''8314'__20 → T_Tree_166 Source #

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

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

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

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

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

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

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

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

d_headTail_634 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_166 → T_Σ_14 Source #

du_headTail_634 ∷ Integer → T_Tree_166 → T_Σ_14 Source #

d_initLast_684 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_166 → T_Σ_14 Source #

du_initLast_684 ∷ Integer → T_Tree_166 → T_Σ_14 Source #

d_join_740 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → Integer → Integer → T_Tree_166 → T_Tree_166 → T__'8764'_'8852'__30 → T_Σ_14 Source #

du_join_740 ∷ T_StrictTotalOrder_864 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → Integer → Integer → T_Tree_166 → T_Tree_166 → T__'8764'_'8852'__30 → T_Σ_14 Source #

d_empty_776 ∷ T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T_Tree_166 Source #

du_empty_776 ∷ T__'60''8314'__20 → T_Tree_166 Source #

d_singleton_784 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → AgdaAny → AgdaAny → T_Σ_14 → T_Tree_166 Source #

du_singleton_784 ∷ AgdaAny → AgdaAny → T_Σ_14 → T_Tree_166 Source #

d_insertWith_804 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → AgdaAny → (Maybe AgdaAny → AgdaAny) → T_Tree_166 → T_Σ_14 → T_Σ_14 Source #

du_insertWith_804 ∷ T_StrictTotalOrder_864 → T_Value_38 → AgdaAny → (Maybe AgdaAny → AgdaAny) → T_Tree_166 → T_Σ_14 → T_Σ_14 Source #

d_insert_906 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → AgdaAny → AgdaAny → T_Tree_166 → T_Σ_14 → T_Σ_14 Source #

du_insert_906 ∷ T_StrictTotalOrder_864 → T_Value_38 → AgdaAny → AgdaAny → T_Tree_166 → T_Σ_14 → T_Σ_14 Source #

d_delete_922 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → AgdaAny → T_Tree_166 → T_Σ_14 → T_Σ_14 Source #

du_delete_922 ∷ T_StrictTotalOrder_864 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → AgdaAny → T_Tree_166 → T_Σ_14 → T_Σ_14 Source #

d_lookup_1020 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → AgdaAny → T_Tree_166 → T_Σ_14 → Maybe AgdaAny Source #

du_lookup_1020 ∷ T_StrictTotalOrder_864 → T_Value_38 → AgdaAny → T_Tree_166 → T_Σ_14 → Maybe AgdaAny Source #

d_foldr_1100 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → T_Level_18 → () → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Tree_166 → AgdaAny Source #

du_foldr_1100 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Tree_166 → AgdaAny Source #

d_toDiffList_1126 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_166 → [T_K'38'__56] → [T_K'38'__56] Source #

du_toDiffList_1126 ∷ T_Tree_166 → [T_K'38'__56] → [T_K'38'__56] Source #

d_toList_1140 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_166 → [T_K'38'__56] Source #

du_toList_1140 ∷ T_Tree_166 → [T_K'38'__56] Source #

d_size_1150 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_Level_18 → T_Value_38 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_166 → Integer Source #

du_size_1150 ∷ T_Tree_166 → Integer Source #

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

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

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

du_map_1174 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_Tree_166 → T_Tree_166 Source #