Safe HaskellNone

MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Properties

Documentation

d_'8759''45'injective'737'_46 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> [AgdaAny] -> [AgdaAny] -> AgdaAny -> AgdaAny -> T_Sublist_26 -> T_Sublist_26 -> T__'8801'__12 -> T__'8801'__12 Source #

d_'8759''45'injective'691'_64 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> [AgdaAny] -> [AgdaAny] -> AgdaAny -> AgdaAny -> T_Sublist_26 -> T_Sublist_26 -> T__'8801'__12 -> T__'8801'__12 Source #

d_'8759''691''45'injective_76 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T__'8801'__12 -> T__'8801'__12 Source #

d_length'45'mono'45''8804'_98 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T__'8804'__18 Source #

du_length'45'mono'45''8804'_98 :: [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T__'8804'__18 Source #

d_fromPointwise_108 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Sublist_26 Source #

du_fromPointwise_108 :: [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Sublist_26 Source #

d_toPointwise_118 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> T__'8801'__12 -> T_Sublist_26 -> T_Pointwise_48 Source #

du_toPointwise_118 :: [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Pointwise_48 Source #

d_tail'45'Sublist_162 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_All_18 Source #

du_tail'45'Sublist_162 :: [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_All_18 Source #

d_take'45'Sublist_180 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> Integer -> T_Sublist_26 -> T_Sublist_26 Source #

du_take'45'Sublist_180 :: [AgdaAny] -> [AgdaAny] -> Integer -> T_Sublist_26 -> T_Sublist_26 Source #

d_drop'45'Sublist_200 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> Integer -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

du_drop'45'Sublist_200 :: Integer -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

d_takeWhile'45'Sublist_244 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> T_Dec_32) -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

du_takeWhile'45'Sublist_244 :: (AgdaAny -> T_Dec_32) -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

d_dropWhile'45'Sublist_282 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> T_Dec_32) -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

du_dropWhile'45'Sublist_282 :: (AgdaAny -> T_Dec_32) -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

d_filter'45'Sublist_320 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> T_Dec_32) -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

du_filter'45'Sublist_320 :: (AgdaAny -> T_Dec_32) -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

d_'8759''737''8315'_376 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

du_'8759''737''8315'_376 :: [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

d_'8759''691''8315'_394 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> [AgdaAny] -> AgdaAny -> [AgdaAny] -> (AgdaAny -> T_'8869'_4) -> T_Sublist_26 -> T_Sublist_26 Source #

du_'8759''691''8315'_394 :: T_Sublist_26 -> T_Sublist_26 Source #

d_'8759''8315'_416 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> [AgdaAny] -> AgdaAny -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

du_'8759''8315'_416 :: [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

d_map'8314'_462 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Sublist_26 -> T_Sublist_26 Source #

du_map'8314'_462 :: [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

d_map'8315'_496 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Sublist_26 -> T_Sublist_26 Source #

du_map'8315'_496 :: [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

d_'43''43''8314'_560 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 Source #

du_'43''43''8314'_560 :: [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 Source #

d_'43''43''8315'_584 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T__'8801'__12 -> T_Sublist_26 -> T_Sublist_26 Source #

du_'43''43''8315'_584 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

d_'43''43''737'_608 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

du_'43''43''737'_608 :: [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

d_'43''43''691'_618 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

du_'43''43''691'_618 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

d_concat'8314'_638 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [[AgdaAny]] -> [[AgdaAny]] -> T_Sublist_26 -> T_Sublist_26 Source #

du_concat'8314'_638 :: [[AgdaAny]] -> [[AgdaAny]] -> T_Sublist_26 -> T_Sublist_26 Source #

d_take'8314'_656 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> Integer -> Integer -> [AgdaAny] -> [AgdaAny] -> T__'8804'__18 -> T_Pointwise_48 -> T_Sublist_26 Source #

du_take'8314'_656 :: Integer -> [AgdaAny] -> [AgdaAny] -> T__'8804'__18 -> T_Pointwise_48 -> T_Sublist_26 Source #

d_drop'8314'_676 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> Integer -> Integer -> [AgdaAny] -> [AgdaAny] -> T__'8804'__18 -> T_Sublist_26 -> T_Sublist_26 Source #

du_drop'8314'_676 :: Integer -> [AgdaAny] -> [AgdaAny] -> T__'8804'__18 -> T_Sublist_26 -> T_Sublist_26 Source #

d_drop'8314''45''8805'_704 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> Integer -> Integer -> [AgdaAny] -> [AgdaAny] -> T__'8804'__18 -> T_Pointwise_48 -> T_Sublist_26 Source #

du_drop'8314''45''8805'_704 :: Integer -> [AgdaAny] -> [AgdaAny] -> T__'8804'__18 -> T_Pointwise_48 -> T_Sublist_26 Source #

d_drop'8314''45''8838'_716 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> Integer -> T_Sublist_26 -> T_Sublist_26 Source #

du_drop'8314''45''8838'_716 :: [AgdaAny] -> [AgdaAny] -> Integer -> T_Sublist_26 -> T_Sublist_26 Source #

d_'8838''45'takeWhile'45'Sublist_756 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> T_Dec_32) -> (AgdaAny -> T_Dec_32) -> [AgdaAny] -> [AgdaAny] -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Pointwise_48 -> T_Sublist_26 Source #

du_'8838''45'takeWhile'45'Sublist_756 :: (AgdaAny -> T_Dec_32) -> (AgdaAny -> T_Dec_32) -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Sublist_26 Source #

d_'8839''45'dropWhile'45'Sublist_832 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> T_Dec_32) -> (AgdaAny -> T_Dec_32) -> [AgdaAny] -> [AgdaAny] -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Pointwise_48 -> T_Sublist_26 Source #

du_'8839''45'dropWhile'45'Sublist_832 :: (AgdaAny -> T_Dec_32) -> (AgdaAny -> T_Dec_32) -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Sublist_26 Source #

d_'8838''45'filter'45'Sublist_922 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> T_Dec_32) -> (AgdaAny -> T_Dec_32) -> [AgdaAny] -> [AgdaAny] -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Sublist_26 -> T_Sublist_26 Source #

du_'8838''45'filter'45'Sublist_922 :: (AgdaAny -> T_Dec_32) -> (AgdaAny -> T_Dec_32) -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

d_takeWhile'45'filter_1046 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> T_Dec_32) -> [AgdaAny] -> T_Pointwise_48 -> T_Sublist_26 Source #

du_takeWhile'45'filter_1046 :: (AgdaAny -> T_Dec_32) -> [AgdaAny] -> T_Pointwise_48 -> T_Sublist_26 Source #

d_filter'45'dropWhile_1078 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> T_Dec_32) -> [AgdaAny] -> T_Pointwise_48 -> T_Sublist_26 Source #

du_filter'45'dropWhile_1078 :: (AgdaAny -> T_Dec_32) -> [AgdaAny] -> T_Pointwise_48 -> T_Sublist_26 Source #

d_reverseAcc'8314'_1132 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 Source #

du_reverseAcc'8314'_1132 :: [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 Source #

d_'691''43''43''8314'_1156 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 Source #

du_'691''43''43''8314'_1156 :: [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 Source #

d_reverse'8314'_1162 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

du_reverse'8314'_1162 :: [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

d_reverse'8315'_1170 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

du_reverse'8315'_1170 :: [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

d_cast_1182 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 Source #

du_cast_1182 :: T_Sublist_26 -> T_Sublist_26 Source #

d_'8759''8315''185'_1208 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> [AgdaAny] -> AgdaAny -> [AgdaAny] -> AgdaAny -> T_Equivalence_928 Source #

du_'8759''8315''185'_1208 :: [AgdaAny] -> AgdaAny -> T_Equivalence_928 Source #

d_'8759''691''8315''185'_1214 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> [AgdaAny] -> AgdaAny -> [AgdaAny] -> (AgdaAny -> T_'8869'_4) -> T_Equivalence_928 Source #

du_'8759''691''8315''185'_1214 :: T_Equivalence_928 Source #

d_Sublist'45''91''93''45'irrelevant_1236 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T__'8801'__12 Source #

d_toAny'45'injective_1254 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> AgdaAny -> T_Sublist_26 -> T_Sublist_26 -> T__'8801'__12 -> T__'8801'__12 Source #

d_fromAny'45'injective_1276 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> AgdaAny -> T_Any_34 -> T_Any_34 -> T__'8801'__12 -> T__'8801'__12 Source #

d_toAny'8728'fromAny'8791'id_1292 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> AgdaAny -> T_Any_34 -> T__'8801'__12 Source #

d_Sublist'45''91'x'93''45'bijection_1302 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> [AgdaAny] -> T_Bijection_844 Source #

du_Sublist'45''91'x'93''45'bijection_1302 :: [AgdaAny] -> T_Bijection_844 Source #

d_reflexive_1316 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> T__'8801'__12 -> T_Sublist_26 Source #

du_reflexive_1316 :: (AgdaAny -> AgdaAny) -> [AgdaAny] -> T_Sublist_26 Source #

d_refl_1318 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> [AgdaAny] -> T_Sublist_26 Source #

du_refl_1318 :: (AgdaAny -> AgdaAny) -> [AgdaAny] -> T_Sublist_26 Source #

d_trans_1348 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 Source #

du_trans_1348 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 Source #

d_antisym_1396 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Pointwise_48 Source #

du_antisym_1396 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Pointwise_48 Source #

d_sublist'63'_1478 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Dec_32) -> [AgdaAny] -> [AgdaAny] -> T_Dec_32 Source #

du_sublist'63'_1478 :: (AgdaAny -> AgdaAny -> T_Dec_32) -> [AgdaAny] -> [AgdaAny] -> T_Dec_32 Source #

d_isPreorder_1534 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> T_IsPreorder_70 Source #

du_isPreorder_1534 :: T_IsPreorder_70 -> T_IsPreorder_70 Source #

d_isPartialOrder_1570 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_162 -> T_IsPartialOrder_162 Source #

du_isPartialOrder_1570 :: T_IsPartialOrder_162 -> T_IsPartialOrder_162 Source #

d_isDecPartialOrder_1610 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_206 -> T_IsDecPartialOrder_206 Source #

du_isDecPartialOrder_1610 :: T_IsDecPartialOrder_206 -> T_IsDecPartialOrder_206 Source #

d_preorder_1672 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Preorder_132 -> T_Preorder_132 Source #

du_preorder_1672 :: T_Preorder_132 -> T_Preorder_132 Source #

d_poset_1728 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Poset_282 -> T_Poset_282 Source #

du_poset_1728 :: T_Poset_282 -> T_Poset_282 Source #

d_decPoset_1790 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DecPoset_360 -> T_DecPoset_360 Source #

du_decPoset_1790 :: T_DecPoset_360 -> T_DecPoset_360 Source #

d__'8838'__1880 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> () Source #

d_DisjointUnion'8594'Disjoint_1896 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> T_DisjointUnion_198 -> T_Disjoint_130 Source #

du_DisjointUnion'8594'Disjoint_1896 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> T_DisjointUnion_198 -> T_Disjoint_130 Source #

d_Disjoint'8594'DisjointUnion_1924 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Disjoint_130 -> T_Σ_14 Source #

du_Disjoint'8594'DisjointUnion_1924 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Disjoint_130 -> T_Σ_14 Source #

d_'8838''45'disjoint'63'_1948 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Dec_32 Source #

du_'8838''45'disjoint'63'_1948 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Dec_32 Source #

d_Disjoint'45'irrelevant_2004 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Disjoint_130 -> T_Disjoint_130 -> T__'8801'__12 Source #

d_Disjoint'45'irrefl'8242'_2036 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Disjoint_130 -> T_All_44 Source #

du_Disjoint'45'irrefl'8242'_2036 :: [AgdaAny] -> T_Sublist_26 -> T_Disjoint_130 -> T_All_44 Source #

d_Disjoint'45'irrefl_2048 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T__'8801'__12 -> T_Disjoint_130 -> T_'8869'_4 Source #

d_DisjointUnion'45'sym_2072 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> T_DisjointUnion_198 -> T_DisjointUnion_198 Source #

du_DisjointUnion'45'sym_2072 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> T_DisjointUnion_198 -> T_DisjointUnion_198 Source #

d_Disjoint'45'sym_2096 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Disjoint_130 -> T_Disjoint_130 Source #

du_Disjoint'45'sym_2096 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Disjoint_130 -> T_Disjoint_130 Source #

d_DisjointUnion'45''91''93''737'_2118 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_DisjointUnion_198 Source #

du_DisjointUnion'45''91''93''737'_2118 :: [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_DisjointUnion_198 Source #

d_DisjointUnion'45''91''93''691'_2142 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_DisjointUnion_198 Source #

du_DisjointUnion'45''91''93''691'_2142 :: [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_DisjointUnion_198 Source #

d_DisjointUnion'45'fromAny'8728'toAny'45''8759''737''8315'_2166 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_DisjointUnion_198 Source #

du_DisjointUnion'45'fromAny'8728'toAny'45''8759''737''8315'_2166 :: [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_DisjointUnion_198 Source #

d_DisjointUnion'179'_2202 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> p10 -> p11 -> p12 -> p13 -> p14 -> p15 -> p16 -> p17 -> p18 -> p19 -> () Source #

data T_DisjointUnion'179'_2202 Source #

Constructors

C_DisjointUnion'179''46'constructor_450417 [AgdaAny] T_Sublist_26 T_DisjointUnion_198 T_DisjointUnion_198 T_DisjointUnion_198 

d_union'179'_2240 :: T_DisjointUnion'179'_2202 -> [AgdaAny] Source #

d_sub'179'_2242 :: T_DisjointUnion'179'_2202 -> T_Sublist_26 Source #

d_join'8321'_2244 :: T_DisjointUnion'179'_2202 -> T_DisjointUnion_198 Source #

d_join'8322'_2246 :: T_DisjointUnion'179'_2202 -> T_DisjointUnion_198 Source #

d_join'8323'_2248 :: T_DisjointUnion'179'_2202 -> T_DisjointUnion_198 Source #

d__'8759''691''45'DisjointUnion'179'__2278 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> T_DisjointUnion'179'_2202 -> T_DisjointUnion'179'_2202 Source #

du__'8759''691''45'DisjointUnion'179'__2278 :: T_DisjointUnion'179'_2202 -> T_DisjointUnion'179'_2202 Source #

d__'8759''8321''45'DisjointUnion'179'__2322 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> AgdaAny -> AgdaAny -> T_DisjointUnion'179'_2202 -> T_DisjointUnion'179'_2202 Source #

du__'8759''8321''45'DisjointUnion'179'__2322 :: AgdaAny -> AgdaAny -> T_DisjointUnion'179'_2202 -> T_DisjointUnion'179'_2202 Source #

d__'8759''8322''45'DisjointUnion'179'__2366 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> AgdaAny -> AgdaAny -> T_DisjointUnion'179'_2202 -> T_DisjointUnion'179'_2202 Source #

du__'8759''8322''45'DisjointUnion'179'__2366 :: AgdaAny -> AgdaAny -> T_DisjointUnion'179'_2202 -> T_DisjointUnion'179'_2202 Source #

d__'8759''8323''45'DisjointUnion'179'__2410 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> AgdaAny -> AgdaAny -> T_DisjointUnion'179'_2202 -> T_DisjointUnion'179'_2202 Source #

du__'8759''8323''45'DisjointUnion'179'__2410 :: AgdaAny -> AgdaAny -> T_DisjointUnion'179'_2202 -> T_DisjointUnion'179'_2202 Source #

d_disjointUnion'179'_2448 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> T_DisjointUnion_198 -> T_DisjointUnion_198 -> T_DisjointUnion_198 -> T_DisjointUnion'179'_2202 Source #

du_disjointUnion'179'_2448 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> T_DisjointUnion_198 -> T_DisjointUnion_198 -> T_DisjointUnion_198 -> T_DisjointUnion'179'_2202 Source #

d_disjoint'8658'disjoint'45'to'45'union_2514 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> T_Disjoint_130 -> T_Disjoint_130 -> T_DisjointUnion_198 -> T_Disjoint_130 Source #

du_disjoint'8658'disjoint'45'to'45'union_2514 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> T_Disjoint_130 -> T_Disjoint_130 -> T_DisjointUnion_198 -> T_Disjoint_130 Source #

d_weakenDisjointUnion_2572 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> T_DisjointUnion_198 -> T_DisjointUnion_198 Source #

du_weakenDisjointUnion_2572 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> T_DisjointUnion_198 -> T_DisjointUnion_198 Source #

d_weakenDisjoint_2616 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> T_Disjoint_130 -> T_Disjoint_130 Source #

du_weakenDisjoint_2616 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> T_Disjoint_130 -> T_Disjoint_130 Source #

d_shrinkDisjoint_2664 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> T_Disjoint_130 -> T_Disjoint_130 Source #

du_shrinkDisjoint_2664 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 -> T_Disjoint_130 -> T_Disjoint_130 Source #