| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Construct.Add.Extrema.Strict
Documentation
d__'60''8331'__22 ∷ p → p → p → p → p → p → () Source #
d__'60''8314'__88 ∷ p → p → p → p → p → p → () Source #
d_'91''60''93''45'injective_164 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T__'60''8314'__20 → AgdaAny Source #
d_'60''177''45'asym_166 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T__'60''8314'__20 → T_Irrelevant_20 Source #
d_'60''177''45'trans_168 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
du_'60''177''45'trans_168 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
d_'60''177''45'dec_170 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_Dec_20 Source #
du_'60''177''45'dec_170 ∷ (AgdaAny → AgdaAny → T_Dec_20) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_Dec_20 Source #
d_'60''177''45'irrelevant_172 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T__'60''8314'__20 → T__'8801'__12 Source #
d__'8804''8314'__184 ∷ p → p → p → p → p → p → p → p → () Source #
d_'60''177''45'trans'691'_238 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8804''8314'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
du_'60''177''45'trans'691'_238 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8804''8314'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
d_'60''177''45'trans'737'_240 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T__'8804''8314'__20 → T__'60''8314'__20 Source #
du_'60''177''45'trans'737'_240 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T__'8804''8314'__20 → T__'60''8314'__20 Source #
d_'60''177''45'cmp'45''8801'_242 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Tri_158) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_Tri_158 Source #
du_'60''177''45'cmp'45''8801'_242 ∷ (AgdaAny → AgdaAny → T_Tri_158) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_Tri_158 Source #
d_'60''177''45'irrefl'45''8801'_244 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → T_Irrelevant_20) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8801'__12 → T__'60''8314'__20 → T_Irrelevant_20 Source #
d_'60''177''45'resp'737''45''8801'_246 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8801'__12 → T__'60''8314'__20 → T__'60''8314'__20 Source #
d_'60''177''45'resp'691''45''8801'_248 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8801'__12 → T__'60''8314'__20 → T__'60''8314'__20 Source #
d_'60''177''45'resp'45''8801'_250 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Σ_14 Source #
d__'8776''8729'__262 ∷ p → p → p → p → p → p → p → p → () Source #
d_'60''177''45'cmp_288 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Tri_158) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_Tri_158 Source #
du_'60''177''45'cmp_288 ∷ (AgdaAny → AgdaAny → T_Tri_158) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_Tri_158 Source #
d_'60''177''45'irrefl_290 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 → T__'60''8314'__20 → T_Irrelevant_20 Source #
d_'60''177''45'resp'737''45''8776''177'_292 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
du_'60''177''45'resp'737''45''8776''177'_292 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
d_'60''177''45'resp'691''45''8776''177'_294 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
du_'60''177''45'resp'691''45''8776''177'_294 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
d_'60''177''45'resp'45''8776''177'_296 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #
d_'60''177''45'isStrictPartialOrder'45''8801'_298 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_370 → T_IsStrictPartialOrder_370 Source #
du_'60''177''45'isStrictPartialOrder'45''8801'_298 ∷ T_IsStrictPartialOrder_370 → T_IsStrictPartialOrder_370 Source #
d_'60''177''45'isDecStrictPartialOrder'45''8801'_300 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_418 → T_IsDecStrictPartialOrder_418 Source #
du_'60''177''45'isDecStrictPartialOrder'45''8801'_300 ∷ T_IsDecStrictPartialOrder_418 → T_IsDecStrictPartialOrder_418 Source #
d_'60''177''45'isStrictTotalOrder'45''8801'_302 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → T_IsStrictTotalOrder_624 Source #
du_'60''177''45'isStrictTotalOrder'45''8801'_302 ∷ T_IsStrictTotalOrder_624 → T_IsStrictTotalOrder_624 Source #
d__'8776''8729'__314 ∷ p → p → p → p → p → p → p → p → () Source #
d_'60''177''45'isStrictPartialOrder_340 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_370 → T_IsStrictPartialOrder_370 Source #
du_'60''177''45'isStrictPartialOrder_340 ∷ T_IsStrictPartialOrder_370 → T_IsStrictPartialOrder_370 Source #
d_'60''177''45'isDecStrictPartialOrder_342 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_418 → T_IsDecStrictPartialOrder_418 Source #
du_'60''177''45'isDecStrictPartialOrder_342 ∷ T_IsDecStrictPartialOrder_418 → T_IsDecStrictPartialOrder_418 Source #
d_'60''177''45'isStrictTotalOrder_344 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → T_IsStrictTotalOrder_624 Source #