| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict
Documentation
d__'60''8331'__20 ∷ p → p → p → p → p → p → () Source #
data T__'60''8331'__20 Source #
Constructors
| C_'8869''8331''60''91'_'93'_24 | |
| C_'91'_'93'_30 AgdaAny |
d_'91''60''93''45'injective_36 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T__'60''8331'__20 → AgdaAny Source #
d_'60''8331''45'asym_40 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → Maybe AgdaAny → Maybe AgdaAny → T__'60''8331'__20 → T__'60''8331'__20 → T_Irrelevant_20 Source #
d_'60''8331''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''8331'__20 → T__'60''8331'__20 → T__'60''8331'__20 Source #
du_'60''8331''45'trans_48 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'60''8331'__20 → T__'60''8331'__20 → T__'60''8331'__20 Source #
d_'60''8331''45'dec_62 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → Maybe AgdaAny → Maybe AgdaAny → T_Dec_20 Source #
du_'60''8331''45'dec_62 ∷ (AgdaAny → AgdaAny → T_Dec_20) → Maybe AgdaAny → Maybe AgdaAny → T_Dec_20 Source #
d_'60''8331''45'irrelevant_80 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12) → Maybe AgdaAny → Maybe AgdaAny → T__'60''8331'__20 → T__'60''8331'__20 → T__'8801'__12 Source #
d__'8804''8331'__102 ∷ p → p → p → p → p → p → p → p → () Source #
d_'60''8331''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''8331'__20 → T__'60''8331'__20 → T__'60''8331'__20 Source #
du_'60''8331''45'trans'691'_154 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'8804''8331'__20 → T__'60''8331'__20 → T__'60''8331'__20 Source #
d_'60''8331''45'trans'737'_170 ∷ 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''8331'__20 → T__'8804''8331'__20 → T__'60''8331'__20 Source #
du_'60''8331''45'trans'737'_170 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'60''8331'__20 → T__'8804''8331'__20 → T__'60''8331'__20 Source #
d_'60''8331''45'accessible'45''8869''8331'_182 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Acc_42 Source #
d_'60''8331''45'accessible'91'_'93'_186 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → T_Acc_42 → T_Acc_42 Source #
d_wf'45'acc_194 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T_Acc_42 → Maybe AgdaAny → T__'60''8331'__20 → T_Acc_42 Source #
d_'60''8331''45'wellFounded_200 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → Maybe AgdaAny → T_Acc_42 Source #
d_'60''8331''45'cmp'45''8801'_208 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Tri_158) → Maybe AgdaAny → Maybe AgdaAny → T_Tri_158 Source #
du_'60''8331''45'cmp'45''8801'_208 ∷ (AgdaAny → AgdaAny → T_Tri_158) → Maybe AgdaAny → Maybe AgdaAny → T_Tri_158 Source #
d_'60''8331''45'irrefl'45''8801'_264 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → T_Irrelevant_20) → Maybe AgdaAny → Maybe AgdaAny → T__'8801'__12 → T__'60''8331'__20 → T_Irrelevant_20 Source #
d_'60''8331''45'resp'737''45''8801'_270 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'8801'__12 → T__'60''8331'__20 → T__'60''8331'__20 Source #
d_'60''8331''45'resp'691''45''8801'_274 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'8801'__12 → T__'60''8331'__20 → T__'60''8331'__20 Source #
d_'60''8331''45'resp'45''8801'_278 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Σ_14 Source #
d__'8776''8729'__290 ∷ p → p → p → p → p → p → p → p → () Source #
d_'60''8331''45'cmp_312 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Tri_158) → Maybe AgdaAny → Maybe AgdaAny → T_Tri_158 Source #
du_'60''8331''45'cmp_312 ∷ (AgdaAny → AgdaAny → T_Tri_158) → Maybe AgdaAny → Maybe AgdaAny → T_Tri_158 Source #
d_'60''8331''45'irrefl_370 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → Maybe AgdaAny → Maybe AgdaAny → T__'8776''8729'__20 → T__'60''8331'__20 → T_Irrelevant_20 Source #
d_'60''8331''45'resp'737''45''8776''8331'_378 ∷ 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''8331'__20 → T__'60''8331'__20 Source #
du_'60''8331''45'resp'737''45''8776''8331'_378 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'8776''8729'__20 → T__'60''8331'__20 → T__'60''8331'__20 Source #
d_'60''8331''45'resp'691''45''8776''8331'_390 ∷ 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''8331'__20 → T__'60''8331'__20 Source #
du_'60''8331''45'resp'691''45''8776''8331'_390 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'8776''8729'__20 → T__'60''8331'__20 → T__'60''8331'__20 Source #
d_'60''8331''45'resp'45''8776''8331'_408 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #
d_'60''8331''45'isStrictPartialOrder'45''8801'_410 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_370 → T_IsStrictPartialOrder_370 Source #
du_'60''8331''45'isStrictPartialOrder'45''8801'_410 ∷ T_IsStrictPartialOrder_370 → T_IsStrictPartialOrder_370 Source #
d_'60''8331''45'isDecStrictPartialOrder'45''8801'_446 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_418 → T_IsDecStrictPartialOrder_418 Source #
du_'60''8331''45'isDecStrictPartialOrder'45''8801'_446 ∷ T_IsDecStrictPartialOrder_418 → T_IsDecStrictPartialOrder_418 Source #
d_'60''8331''45'isStrictTotalOrder'45''8801'_494 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → T_IsStrictTotalOrder_624 Source #
du_'60''8331''45'isStrictTotalOrder'45''8801'_494 ∷ T_IsStrictTotalOrder_624 → T_IsStrictTotalOrder_624 Source #
d__'8776''8729'__558 ∷ p → p → p → p → p → p → p → p → () Source #
d_'60''8331''45'isStrictPartialOrder_580 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_370 → T_IsStrictPartialOrder_370 Source #
du_'60''8331''45'isStrictPartialOrder_580 ∷ T_IsStrictPartialOrder_370 → T_IsStrictPartialOrder_370 Source #
d_'60''8331''45'isDecStrictPartialOrder_616 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_418 → T_IsDecStrictPartialOrder_418 Source #
du_'60''8331''45'isDecStrictPartialOrder_616 ∷ T_IsDecStrictPartialOrder_418 → T_IsDecStrictPartialOrder_418 Source #
d_'60''8331''45'isStrictTotalOrder_664 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → T_IsStrictTotalOrder_624 Source #