| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.NonStrict
Documentation
d__'8804''8331'__20 ∷ p → p → p → p → p → p → () Source #
data T__'8804''8331'__20 Source #
Constructors
| C_'8869''8331''8804'__24 | |
| C_'91'_'93'_30 AgdaAny |
d_'91''8804''93''45'injective_36 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T__'8804''8331'__20 → AgdaAny Source #
d_'8804''8331''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''8331'__20 → T__'8804''8331'__20 → T__'8804''8331'__20 Source #
du_'8804''8331''45'trans_40 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'8804''8331'__20 → T__'8804''8331'__20 → T__'8804''8331'__20 Source #
d_'8804''8331''45'minimum_54 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → Maybe AgdaAny → T__'8804''8331'__20 Source #
d_'8804''8331''45'dec_56 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → Maybe AgdaAny → Maybe AgdaAny → T_Dec_32 Source #
du_'8804''8331''45'dec_56 ∷ (AgdaAny → AgdaAny → T_Dec_32) → Maybe AgdaAny → Maybe AgdaAny → T_Dec_32 Source #
d_'8804''8331''45'total_72 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T__'8846'__30) → Maybe AgdaAny → Maybe AgdaAny → T__'8846'__30 Source #
du_'8804''8331''45'total_72 ∷ (AgdaAny → AgdaAny → T__'8846'__30) → Maybe AgdaAny → Maybe AgdaAny → T__'8846'__30 Source #
d_'8804''8331''45'irrelevant_88 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12) → Maybe AgdaAny → Maybe AgdaAny → T__'8804''8331'__20 → T__'8804''8331'__20 → T__'8801'__12 Source #
d_'8804''8331''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''8331'__20 Source #
du_'8804''8331''45'reflexive'45''8801'_100 ∷ (AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny) → Maybe AgdaAny → T__'8804''8331'__20 Source #
d_'8804''8331''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''8331'__20 → T__'8804''8331'__20 → T__'8801'__12 Source #
d__'8776''8729'__128 ∷ p → p → p → p → p → p → p → p → () Source #
d_'8804''8331''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''8331'__20 Source #
du_'8804''8331''45'reflexive_158 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → Maybe AgdaAny → T__'8776''8729'__20 → T__'8804''8331'__20 Source #
d_'8804''8331''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''8331'__20 → T__'8804''8331'__20 → T__'8776''8729'__20 Source #
du_'8804''8331''45'antisym_166 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → Maybe AgdaAny → T__'8804''8331'__20 → T__'8804''8331'__20 → T__'8776''8729'__20 Source #
d_'8804''8331''45'isPreorder'45''8801'_176 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsPreorder_70 → T_IsPreorder_70 Source #
d_'8804''8331''45'isPartialOrder'45''8801'_212 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_162 → T_IsPartialOrder_162 Source #
du_'8804''8331''45'isPartialOrder'45''8801'_212 ∷ T_IsPartialOrder_162 → T_IsPartialOrder_162 Source #
d_'8804''8331''45'isDecPartialOrder'45''8801'_252 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_206 → T_IsDecPartialOrder_206 Source #
du_'8804''8331''45'isDecPartialOrder'45''8801'_252 ∷ T_IsDecPartialOrder_206 → T_IsDecPartialOrder_206 Source #
d_'8804''8331''45'isTotalOrder'45''8801'_304 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_384 → T_IsTotalOrder_384 Source #
d_'8804''8331''45'isDecTotalOrder'45''8801'_350 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_434 → T_IsDecTotalOrder_434 Source #
du_'8804''8331''45'isDecTotalOrder'45''8801'_350 ∷ T_IsDecTotalOrder_434 → T_IsDecTotalOrder_434 Source #
d__'8776''8729'__420 ∷ p → p → p → p → p → p → p → p → () Source #
d_'8804''8331''45'isPreorder_450 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPreorder_70 → T_IsPreorder_70 Source #
d_'8804''8331''45'isPartialOrder_486 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_162 → T_IsPartialOrder_162 Source #
d_'8804''8331''45'isDecPartialOrder_526 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_206 → T_IsDecPartialOrder_206 Source #
du_'8804''8331''45'isDecPartialOrder_526 ∷ T_IsDecPartialOrder_206 → T_IsDecPartialOrder_206 Source #
d_'8804''8331''45'isTotalOrder_578 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_384 → T_IsTotalOrder_384 Source #
d_'8804''8331''45'isDecTotalOrder_624 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_434 → T_IsDecTotalOrder_434 Source #