Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Data.Tree.AVL.Indexed

Documentation

d__'60'_'60'__110 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → Maybe (Maybe AgdaAny) → AgdaAny → Maybe (Maybe AgdaAny) → () Source #

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

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

d_Key'8314'_116 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → () Source #

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

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

du_refl'8314'_120 ∷ T_StrictTotalOrder_1280 → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 Source #

d_strictPartialOrder_122 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_StrictPartialOrder_760 Source #

du_strictPartialOrder_122 ∷ T_StrictTotalOrder_1280 → T_StrictPartialOrder_760 Source #

d_strictTotalOrder_124 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_StrictTotalOrder_1280 Source #

du_strictTotalOrder_124 ∷ T_StrictTotalOrder_1280 → T_StrictTotalOrder_1280 Source #

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

du_sym'8314'_126 ∷ T_StrictTotalOrder_1280 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 → T__'8776''8729'__20 Source #

d_trans'8314'_128 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → 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'_128 ∷ T_StrictTotalOrder_1280 → 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'_130 ∷ T_StrictTotalOrder_1280 → AgdaAny → T_Σ_14 Source #

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

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

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

d_Value_158 ∷ p → p → p → p → p → () Source #

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

du_const_162 ∷ T_Level_18 → () → T_Value_40 Source #

d_fromPair_164 ∷ 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_164 ∷ T_Level_18 → T_Value_40 → T_Σ_14 → T_K'38'__58 Source #

d_key_166 ∷ T_K'38'__58 → AgdaAny Source #

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

d_value_170 ∷ T_K'38'__58 → AgdaAny Source #

d_key_174 ∷ T_K'38'__58 → AgdaAny Source #

d_value_176 ∷ T_K'38'__58 → AgdaAny Source #

d_family_180 ∷ T_Value_40 → AgdaAny → () Source #

d_respects_182 ∷ T_Value_40 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Tree_192 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_Tree_192 Source #

Constructors

C_leaf_204 T__'60''8314'__20
C_node_220 Integer Integer T_K'38'__58 T_Tree_192 T_Tree_192 T__'8764'_'8852'__30

d_ordered_236 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_192 → T__'60''8314'__20 Source #

du_ordered_236 ∷ T_StrictTotalOrder_1280 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_Tree_192 → T__'60''8314'__20 Source #

d_Val_248 ∷ T_Value_40 → AgdaAny → () Source #

d_V'8776'_250 ∷ T_Value_40 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_leaf'45'injective_260 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → 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_292 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → Integer → Integer → Integer → Integer → Integer → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_K'38'__58 → T_K'38'__58 → T_Tree_192 → T_Tree_192 → T_Tree_192 → T_Tree_192 → T__'8764'_'8852'__30 → T__'8764'_'8852'__30 → T__'8801'__12 → T__'8801'__12 Source #

d_cast'737'_302 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T__'60''8314'__20 → T_Tree_192 → T_Tree_192 Source #

du_cast'737'_302 ∷ T_StrictTotalOrder_1280 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T_Tree_192 → T_Tree_192 Source #

d_cast'691'_328 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_192 → T__'60''8314'__20 → T_Tree_192 Source #

du_cast'691'_328 ∷ T_StrictTotalOrder_1280 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_Tree_192 → T__'60''8314'__20 → T_Tree_192 Source #

d_join'737''8314'_378 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → Integer → Integer → T_K'38'__58 → T_Σ_14 → T_Tree_192 → T__'8764'_'8852'__30 → T_Σ_14 Source #

du_join'737''8314'_378 ∷ Integer → Integer → T_K'38'__58 → T_Σ_14 → T_Tree_192 → T__'8764'_'8852'__30 → T_Σ_14 Source #

d_join'691''8314'_468 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → Integer → Integer → T_K'38'__58 → T_Tree_192 → T_Σ_14 → T__'8764'_'8852'__30 → T_Σ_14 Source #

du_join'691''8314'_468 ∷ Integer → Integer → T_K'38'__58 → T_Tree_192 → T_Σ_14 → T__'8764'_'8852'__30 → T_Σ_14 Source #

d_join'737''8315'_544 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → Integer → Integer → T_K'38'__58 → T_Σ_14 → T_Tree_192 → T__'8764'_'8852'__30 → T_Σ_14 Source #

du_join'737''8315'_544 ∷ Integer → Integer → T_K'38'__58 → T_Σ_14 → T_Tree_192 → T__'8764'_'8852'__30 → T_Σ_14 Source #

d_join'691''8315'_606 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → Integer → Integer → T_K'38'__58 → T_Tree_192 → T_Σ_14 → T__'8764'_'8852'__30 → T_Σ_14 Source #

du_join'691''8315'_606 ∷ Integer → Integer → T_K'38'__58 → T_Tree_192 → T_Σ_14 → T__'8764'_'8852'__30 → T_Σ_14 Source #

d_headTail_660 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_192 → T_Σ_14 Source #

du_headTail_660 ∷ Integer → T_Tree_192 → T_Σ_14 Source #

d_initLast_710 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_192 → T_Σ_14 Source #

du_initLast_710 ∷ Integer → T_Tree_192 → T_Σ_14 Source #

d_join_766 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → Integer → Integer → T_Tree_192 → T_Tree_192 → T__'8764'_'8852'__30 → T_Σ_14 Source #

du_join_766 ∷ T_StrictTotalOrder_1280 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → Integer → Integer → T_Tree_192 → T_Tree_192 → T__'8764'_'8852'__30 → T_Σ_14 Source #

d_empty_802 ∷ T_Value_40 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T_Tree_192 Source #

du_empty_802 ∷ T__'60''8314'__20 → T_Tree_192 Source #

d_singleton_810 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → AgdaAny → AgdaAny → T_Σ_14 → T_Tree_192 Source #

du_singleton_810 ∷ AgdaAny → AgdaAny → T_Σ_14 → T_Tree_192 Source #

d_insertWith_830 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → AgdaAny → (Maybe AgdaAny → AgdaAny) → T_Tree_192 → T_Σ_14 → T_Σ_14 Source #

du_insertWith_830 ∷ T_StrictTotalOrder_1280 → T_Value_40 → AgdaAny → (Maybe AgdaAny → AgdaAny) → T_Tree_192 → T_Σ_14 → T_Σ_14 Source #

d_insert_932 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → AgdaAny → AgdaAny → T_Tree_192 → T_Σ_14 → T_Σ_14 Source #

du_insert_932 ∷ T_StrictTotalOrder_1280 → T_Value_40 → AgdaAny → AgdaAny → T_Tree_192 → T_Σ_14 → T_Σ_14 Source #

d_delete_948 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → AgdaAny → T_Tree_192 → T_Σ_14 → T_Σ_14 Source #

du_delete_948 ∷ T_StrictTotalOrder_1280 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → AgdaAny → T_Tree_192 → T_Σ_14 → T_Σ_14 Source #

d_lookup_1046 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_192 → AgdaAny → T_Σ_14 → Maybe AgdaAny Source #

du_lookup_1046 ∷ T_StrictTotalOrder_1280 → T_Value_40 → T_Tree_192 → AgdaAny → T_Σ_14 → Maybe AgdaAny Source #

d_foldr_1126 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → T_Level_18 → () → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Tree_192 → AgdaAny Source #

du_foldr_1126 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Tree_192 → AgdaAny Source #

d_toDiffList_1152 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_192 → [T_K'38'__58] → [T_K'38'__58] Source #

du_toDiffList_1152 ∷ T_Tree_192 → [T_K'38'__58] → [T_K'38'__58] Source #

d_toList_1166 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_192 → [T_K'38'__58] Source #

du_toList_1166 ∷ T_Tree_192 → [T_K'38'__58] Source #

d_size_1176 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_Level_18 → T_Value_40 → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Integer → T_Tree_192 → Integer Source #

du_size_1176 ∷ T_Tree_192 → Integer Source #

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

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

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

du_map_1200 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_Tree_192 → T_Tree_192 Source #