| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Construct.NonStrictToStrict
Documentation
d__'8777'__20 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → () Source #
d__'60'__26 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → () Source #
d_'60''8658''8804'_32 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T_Σ_14 → AgdaAny Source #
d_'60''8658''8777'_38 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T_Σ_14 → AgdaAny → T_Irrelevant_20 Source #
d_'8804''8743''8777''8658''60'_44 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → T_Σ_14 Source #
d_'60''8658''8817'_50 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_Σ_14 → AgdaAny → T_Irrelevant_20 Source #
d_'8804''8658''8815'_64 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Irrelevant_20 Source #
d_'8816''8658''62'_76 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → T_Σ_14 Source #
du_'8816''8658''62'_76 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → T_Σ_14 Source #
d_'8814''8658''8805'_126 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → AgdaAny → (T_Σ_14 → T_Irrelevant_20) → AgdaAny Source #
du_'8814''8658''8805'_126 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → AgdaAny → AgdaAny Source #
d_'60''45'irrefl_196 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Irrelevant_20 Source #
d_'60''45'trans_202 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_248 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
du_'60''45'trans_202 ∷ T_IsPartialOrder_248 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'60''45''8804''45'trans_256 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → AgdaAny → T_Σ_14 Source #
du_'60''45''8804''45'trans_256 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → AgdaAny → T_Σ_14 Source #
d_'8804''45''60''45'trans_274 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 Source #
du_'8804''45''60''45'trans_274 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 Source #
d_'60''45'asym_290 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 → T_Irrelevant_20 Source #
d_'60''45'resp'737''45''8776'_300 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 Source #
du_'60''45'resp'737''45''8776'_300 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 Source #
d_'60''45'resp'691''45''8776'_312 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 Source #
du_'60''45'resp'691''45''8776'_312 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 Source #
d_'60''45'resp'45''8776'_328 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_28 → T_Σ_14 → T_Σ_14 Source #
d_'60''45'trichotomous_352 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → AgdaAny → T_Tri_158 Source #
du_'60''45'trichotomous_352 ∷ (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → AgdaAny → T_Tri_158 Source #
d_'60''45'decidable_434 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_Dec_20 Source #
du_'60''45'decidable_434 ∷ (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_Dec_20 Source #
d_'60''45'isStrictPartialOrder_444 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_248 → T_IsStrictPartialOrder_370 Source #
d_'60''45'isDecStrictPartialOrder_490 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_300 → T_IsDecStrictPartialOrder_418 Source #
du_'60''45'isDecStrictPartialOrder_490 ∷ T_IsDecPartialOrder_300 → T_IsDecStrictPartialOrder_418 Source #
d_'60''45'isStrictTotalOrder'8321'_550 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → T_IsTotalOrder_488 → T_IsStrictTotalOrder_624 Source #
du_'60''45'isStrictTotalOrder'8321'_550 ∷ (AgdaAny → AgdaAny → T_Dec_20) → T_IsTotalOrder_488 → T_IsStrictTotalOrder_624 Source #
d_'60''45'isStrictTotalOrder'8322'_604 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_546 → T_IsStrictTotalOrder_624 Source #