plutus-metatheory-1.60.0.0: Command line tool for running plutus core programs
Safe HaskellSafe-Inferred
LanguageHaskell2010

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) -> () #

d__'60''8314'__104 :: p -> p -> p -> p -> p -> p -> () #

d__'8776''8729'__106 :: p -> p -> p -> p -> p -> p -> () #

d_Key'8314'_108 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_StrictTotalOrder_1036 -> () #

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 #

d_refl'8314'_112 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_StrictTotalOrder_1036 -> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20 #

du_refl'8314'_112 :: T_StrictTotalOrder_1036 -> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20 #

d_strictPartialOrder_114 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_StrictTotalOrder_1036 -> T_StrictPartialOrder_556 #

du_strictPartialOrder_114 :: T_StrictTotalOrder_1036 -> T_StrictPartialOrder_556 #

d_strictTotalOrder_116 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_StrictTotalOrder_1036 -> T_StrictTotalOrder_1036 #

du_strictTotalOrder_116 :: T_StrictTotalOrder_1036 -> T_StrictTotalOrder_1036 #

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 #

du_sym'8314'_118 :: T_StrictTotalOrder_1036 -> Maybe (Maybe AgdaAny) -> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20 -> T__'8776''8729'__20 #

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 #

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 #

d_'8869''8314''60''91'_'93''60''8868''8314'_122 :: T_StrictTotalOrder_1036 -> AgdaAny -> T_Σ_14 #

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

d_'91'_'93''45'injective_138 :: T_StrictTotalOrder_1036 -> T_Level_18 -> () -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #

d_K'38'__144 :: p -> p -> p -> p -> p -> p -> () #

d_Value_148 :: p -> p -> p -> p -> p -> () #

d_const_150 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_StrictTotalOrder_1036 -> T_Level_18 -> () -> T_Value_38 #

du_const_150 :: T_Level_18 -> () -> T_Value_38 #

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 #

du_fromPair_152 :: T_Level_18 -> T_Value_38 -> T_Σ_14 -> T_K'38'__56 #

d_key_154 :: T_K'38'__56 -> AgdaAny #

d_toPair_156 :: T_K'38'__56 -> T_Σ_14 #

d_value_158 :: T_K'38'__56 -> AgdaAny #

d_key_162 :: T_K'38'__56 -> AgdaAny #

d_value_164 :: T_K'38'__56 -> AgdaAny #

d_family_168 :: T_Value_38 -> AgdaAny -> () #

d_respects_170 :: T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_Tree_180 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_Tree_180 #

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 #

du_ordered_224 :: T_StrictTotalOrder_1036 -> Maybe (Maybe AgdaAny) -> Maybe (Maybe AgdaAny) -> T_Tree_180 -> T__'60''8314'__20 #

d_Val_236 :: T_Value_38 -> AgdaAny -> () #

d_V'8776'_238 :: T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

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 #

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 #

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 #

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 #

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 #

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 #

du_join'737''8314'_366 :: Integer -> Integer -> T_K'38'__56 -> T_Σ_14 -> T_Tree_180 -> T__'8764'_'8852'__30 -> T_Σ_14 #

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 #

du_join'691''8314'_456 :: Integer -> Integer -> T_K'38'__56 -> T_Tree_180 -> T_Σ_14 -> T__'8764'_'8852'__30 -> T_Σ_14 #

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 #

du_join'737''8315'_532 :: Integer -> Integer -> T_K'38'__56 -> T_Σ_14 -> T_Tree_180 -> T__'8764'_'8852'__30 -> T_Σ_14 #

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 #

du_join'691''8315'_594 :: Integer -> Integer -> T_K'38'__56 -> T_Tree_180 -> T_Σ_14 -> T__'8764'_'8852'__30 -> T_Σ_14 #

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 #

du_headTail_648 :: Integer -> T_Tree_180 -> T_Σ_14 #

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 #

du_initLast_698 :: Integer -> T_Tree_180 -> T_Σ_14 #

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 #

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 #

d_empty_790 :: T_Value_38 -> Maybe (Maybe AgdaAny) -> Maybe (Maybe AgdaAny) -> T__'60''8314'__20 -> T_Tree_180 #

du_empty_790 :: T__'60''8314'__20 -> T_Tree_180 #

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 #

du_singleton_798 :: AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_180 #

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 #

du_insertWith_818 :: T_StrictTotalOrder_1036 -> T_Value_38 -> AgdaAny -> (Maybe AgdaAny -> AgdaAny) -> T_Tree_180 -> T_Σ_14 -> T_Σ_14 #

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 #

du_insert_920 :: T_StrictTotalOrder_1036 -> T_Value_38 -> AgdaAny -> AgdaAny -> T_Tree_180 -> T_Σ_14 -> T_Σ_14 #

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 #

du_delete_936 :: T_StrictTotalOrder_1036 -> Maybe (Maybe AgdaAny) -> Maybe (Maybe AgdaAny) -> Integer -> AgdaAny -> T_Tree_180 -> T_Σ_14 -> T_Σ_14 #

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 #

du_lookup_1034 :: T_StrictTotalOrder_1036 -> T_Value_38 -> T_Tree_180 -> AgdaAny -> T_Σ_14 -> Maybe AgdaAny #

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 #

du_foldr_1114 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Tree_180 -> AgdaAny #

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] #

du_toDiffList_1140 :: T_Tree_180 -> [T_K'38'__56] -> [T_K'38'__56] #

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] #

du_toList_1154 :: T_Tree_180 -> [T_K'38'__56] #

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 #

du_size_1164 :: T_Tree_180 -> Integer #

d_Val_1178 :: T_StrictTotalOrder_1036 -> T_Level_18 -> T_Level_18 -> T_Value_38 -> T_Value_38 -> AgdaAny -> () #

d_Wal_1180 :: T_StrictTotalOrder_1036 -> T_Level_18 -> T_Level_18 -> T_Value_38 -> T_Value_38 -> AgdaAny -> () #

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 #

du_map_1188 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_180 -> T_Tree_180 #