| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.NonStrict
Documentation
d__'8804''8314'__20 :: p -> p -> p -> p -> p -> p -> () #
data T__'8804''8314'__20 #
Constructors
| C_'91'_'93'_26 AgdaAny | |
| C__'8804''8868''8314'_30 |
d_'91''8804''93''45'injective_36 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T__'8804''8314'__20 -> AgdaAny #
d_'8804''8314''45'trans_40 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8804''8314'__20 -> T__'8804''8314'__20 -> T__'8804''8314'__20 #
du_'8804''8314''45'trans_40 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8804''8314'__20 -> T__'8804''8314'__20 -> T__'8804''8314'__20 #
d_'8804''8314''45'maximum_54 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> Maybe AgdaAny -> T__'8804''8314'__20 #
d_'8804''8314''45'dec_56 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Dec_20) -> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_20 #
du_'8804''8314''45'dec_56 :: (AgdaAny -> AgdaAny -> T_Dec_20) -> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_20 #
d_'8804''8314''45'total_72 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8846'__30 #
du_'8804''8314''45'total_72 :: (AgdaAny -> AgdaAny -> T__'8846'__30) -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8846'__30 #
d_'8804''8314''45'irrelevant_88 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12) -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8804''8314'__20 -> T__'8804''8314'__20 -> T__'8801'__12 #
d_'8804''8314''45'reflexive'45''8801'_100 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8801'__12 -> T__'8804''8314'__20 #
du_'8804''8314''45'reflexive'45''8801'_100 :: (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny) -> Maybe AgdaAny -> T__'8804''8314'__20 #
d_'8804''8314''45'antisym'45''8801'_108 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12) -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8804''8314'__20 -> T__'8804''8314'__20 -> T__'8801'__12 #
d__'8776''8729'__128 :: p -> p -> p -> p -> p -> p -> p -> p -> () #
d_'8804''8314''45'reflexive_158 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8776''8729'__20 -> T__'8804''8314'__20 #
du_'8804''8314''45'reflexive_158 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8776''8729'__20 -> T__'8804''8314'__20 #
d_'8804''8314''45'antisym_166 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8804''8314'__20 -> T__'8804''8314'__20 -> T__'8776''8729'__20 #
du_'8804''8314''45'antisym_166 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8804''8314'__20 -> T__'8804''8314'__20 -> T__'8776''8729'__20 #
d_'8804''8314''45'isPreorder'45''8801'_176 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> T_IsPreorder_70 #
d_'8804''8314''45'isPartialOrder'45''8801'_218 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_174 -> T_IsPartialOrder_174 #
d_'8804''8314''45'isDecPartialOrder'45''8801'_264 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_224 -> T_IsDecPartialOrder_224 #
du_'8804''8314''45'isDecPartialOrder'45''8801'_264 :: T_IsDecPartialOrder_224 -> T_IsDecPartialOrder_224 #
d_'8804''8314''45'isTotalOrder'45''8801'_322 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_404 -> T_IsTotalOrder_404 #
d_'8804''8314''45'isDecTotalOrder'45''8801'_374 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_460 -> T_IsDecTotalOrder_460 #
du_'8804''8314''45'isDecTotalOrder'45''8801'_374 :: T_IsDecTotalOrder_460 -> T_IsDecTotalOrder_460 #
d__'8776''8729'__450 :: p -> p -> p -> p -> p -> p -> p -> p -> () #
d_'8804''8314''45'isPreorder_480 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> T_IsPreorder_70 #
d_'8804''8314''45'isPartialOrder_522 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_174 -> T_IsPartialOrder_174 #
d_'8804''8314''45'isDecPartialOrder_568 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_224 -> T_IsDecPartialOrder_224 #
d_'8804''8314''45'isTotalOrder_626 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_404 -> T_IsTotalOrder_404 #
d_'8804''8314''45'isDecTotalOrder_678 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_460 -> T_IsDecTotalOrder_460 #