| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict
Documentation
d__'60''8314'__20 ∷ p → p → p → p → p → p → () Source #
data T__'60''8314'__20 Source #
Constructors
| C_'91'_'93'_26 AgdaAny | |
| C_'91'_'93''60''8868''8314'_30 |
d_'91''60''93''45'injective_36 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T__'60''8314'__20 → AgdaAny Source #
d_'60''8314''45'asym_40 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → Maybe AgdaAny → Maybe AgdaAny → T__'60''8314'__20 → T__'60''8314'__20 → T_'8869'_4 Source #
d_'60''8314''45'trans_48 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'60''8314'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
du_'60''8314''45'trans_48 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'60''8314'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
d_'60''8314''45'dec_62 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → Maybe AgdaAny → Maybe AgdaAny → T_Dec_32 Source #
du_'60''8314''45'dec_62 ∷ (AgdaAny → AgdaAny → T_Dec_32) → Maybe AgdaAny → Maybe AgdaAny → T_Dec_32 Source #
d_'60''8314''45'irrelevant_80 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12) → Maybe AgdaAny → Maybe AgdaAny → T__'60''8314'__20 → T__'60''8314'__20 → T__'8801'__12 Source #
d__'8804''8314'__102 ∷ p → p → p → p → p → p → p → p → () Source #
d_'60''8314''45'trans'691'_154 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'8804''8314'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
du_'60''8314''45'trans'691'_154 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'8804''8314'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
d_'60''8314''45'trans'737'_168 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'60''8314'__20 → T__'8804''8314'__20 → T__'60''8314'__20 Source #
du_'60''8314''45'trans'737'_168 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'60''8314'__20 → T__'8804''8314'__20 → T__'60''8314'__20 Source #
d_'60''8314''45'cmp'45''8801'_184 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Tri_136) → Maybe AgdaAny → Maybe AgdaAny → T_Tri_136 Source #
du_'60''8314''45'cmp'45''8801'_184 ∷ (AgdaAny → AgdaAny → T_Tri_136) → Maybe AgdaAny → Maybe AgdaAny → T_Tri_136 Source #
d_'60''8314''45'irrefl'45''8801'_240 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → T_'8869'_4) → Maybe AgdaAny → Maybe AgdaAny → T__'8801'__12 → T__'60''8314'__20 → T_'8869'_4 Source #
d_'60''8314''45'resp'737''45''8801'_246 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'8801'__12 → T__'60''8314'__20 → T__'60''8314'__20 Source #
d_'60''8314''45'resp'691''45''8801'_250 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'8801'__12 → T__'60''8314'__20 → T__'60''8314'__20 Source #
d_'60''8314''45'resp'45''8801'_254 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Σ_14 Source #
d__'8776''8729'__266 ∷ p → p → p → p → p → p → p → p → () Source #
d_'60''8314''45'cmp_296 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Tri_136) → Maybe AgdaAny → Maybe AgdaAny → T_Tri_136 Source #
du_'60''8314''45'cmp_296 ∷ (AgdaAny → AgdaAny → T_Tri_136) → Maybe AgdaAny → Maybe AgdaAny → T_Tri_136 Source #
d_'60''8314''45'irrefl_354 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → Maybe AgdaAny → Maybe AgdaAny → T__'8776''8729'__20 → T__'60''8314'__20 → T_'8869'_4 Source #
d_'60''8314''45'resp'737''45''8776''8314'_362 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'8776''8729'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
du_'60''8314''45'resp'737''45''8776''8314'_362 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'8776''8729'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
d_'60''8314''45'resp'691''45''8776''8314'_380 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'8776''8729'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
du_'60''8314''45'resp'691''45''8776''8314'_380 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'8776''8729'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
d_'60''8314''45'resp'45''8776''8314'_392 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #
d_'60''8314''45'isStrictPartialOrder'45''8801'_394 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 Source #
du_'60''8314''45'isStrictPartialOrder'45''8801'_394 ∷ T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 Source #
d_'60''8314''45'isDecStrictPartialOrder'45''8801'_432 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_314 → T_IsDecStrictPartialOrder_314 Source #
du_'60''8314''45'isDecStrictPartialOrder'45''8801'_432 ∷ T_IsDecStrictPartialOrder_314 → T_IsDecStrictPartialOrder_314 Source #
d_'60''8314''45'isStrictTotalOrder'45''8801'_482 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → T_IsStrictTotalOrder_502 Source #
du_'60''8314''45'isStrictTotalOrder'45''8801'_482 ∷ T_IsStrictTotalOrder_502 → T_IsStrictTotalOrder_502 Source #
d__'8776''8729'__544 ∷ p → p → p → p → p → p → p → p → () Source #
d_'60''8314''45'isStrictPartialOrder_574 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 Source #
du_'60''8314''45'isStrictPartialOrder_574 ∷ T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 Source #
d_'60''8314''45'isDecStrictPartialOrder_612 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_314 → T_IsDecStrictPartialOrder_314 Source #
du_'60''8314''45'isDecStrictPartialOrder_612 ∷ T_IsDecStrictPartialOrder_314 → T_IsDecStrictPartialOrder_314 Source #
d_'60''8314''45'isStrictTotalOrder_662 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → T_IsStrictTotalOrder_502 Source #