| 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_'8869'_4 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_'8869'_4) → 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_'8869'_4 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_'8869'_4 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_'8869'_4) → 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_'8869'_4) → 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_32) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → AgdaAny → (T_Σ_14 → T_'8869'_4) → AgdaAny Source #
du_'8814''8658''8805'_126 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Dec_32) → (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_'8869'_4 Source #
d_'60''45'trans_202 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_162 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
du_'60''45'trans_202 ∷ T_IsPartialOrder_162 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'60''45''8804''45'trans_250 ∷ 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_250 ∷ (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_268 ∷ 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_268 ∷ (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_284 ∷ 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_'8869'_4 Source #
d_'60''45'resp'737''45''8776'_294 ∷ 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'_294 ∷ (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'_306 ∷ 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'_306 ∷ (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'_322 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → T_Σ_14 → T_Σ_14 Source #
d_'60''45'trichotomous_346 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → AgdaAny → T_Tri_136 Source #
du_'60''45'trichotomous_346 ∷ (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → AgdaAny → T_Tri_136 Source #
d_'60''45'decidable_428 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → T_Dec_32) → AgdaAny → AgdaAny → T_Dec_32 Source #
du_'60''45'decidable_428 ∷ (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → T_Dec_32) → AgdaAny → AgdaAny → T_Dec_32 Source #
d_'60''45'isStrictPartialOrder_438 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_162 → T_IsStrictPartialOrder_266 Source #
d_'60''45'isDecStrictPartialOrder_478 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_206 → T_IsDecStrictPartialOrder_314 Source #
du_'60''45'isDecStrictPartialOrder_478 ∷ T_IsDecPartialOrder_206 → T_IsDecStrictPartialOrder_314 Source #
d_'60''45'isStrictTotalOrder'8321'_530 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → T_IsTotalOrder_384 → T_IsStrictTotalOrder_502 Source #
du_'60''45'isStrictTotalOrder'8321'_530 ∷ (AgdaAny → AgdaAny → T_Dec_32) → T_IsTotalOrder_384 → T_IsStrictTotalOrder_502 Source #
d_'60''45'isStrictTotalOrder'8322'_578 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_434 → T_IsStrictTotalOrder_502 Source #
d_irrefl_638 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_'8869'_4 Source #
d_trans_640 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_162 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
du_trans_640 ∷ T_IsPartialOrder_162 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_antisym'10230'asym_642 ∷ 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_'8869'_4 Source #
d_decidable_644 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → T_Dec_32) → AgdaAny → AgdaAny → T_Dec_32 Source #
du_decidable_644 ∷ (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → T_Dec_32) → AgdaAny → AgdaAny → T_Dec_32 Source #
d_trichotomous_646 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → AgdaAny → T_Tri_136 Source #
du_trichotomous_646 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → AgdaAny → T_Tri_136 Source #
d_isPartialOrder'10230'isStrictPartialOrder_648 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_162 → T_IsStrictPartialOrder_266 Source #
du_isPartialOrder'10230'isStrictPartialOrder_648 ∷ T_IsPartialOrder_162 → T_IsStrictPartialOrder_266 Source #
d_isTotalOrder'10230'isStrictTotalOrder_650 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → T_IsTotalOrder_384 → T_IsStrictTotalOrder_502 Source #
du_isTotalOrder'10230'isStrictTotalOrder_650 ∷ (AgdaAny → AgdaAny → T_Dec_32) → T_IsTotalOrder_384 → T_IsStrictTotalOrder_502 Source #
d_isDecTotalOrder'10230'isStrictTotalOrder_652 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_434 → T_IsStrictTotalOrder_502 Source #