| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.Properties
Documentation
d_'61''91''93''8658'_44 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_ReflClosure_30 → T_ReflClosure_30 Source #
du_'61''91''93''8658'_44 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_ReflClosure_30 → T_ReflClosure_30 Source #
d__'126''7506'__62 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → () Source #
d_fromSum_68 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T__'8846'__30 → T_ReflClosure_30 Source #
d_toSum_76 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T_ReflClosure_30 → T__'8846'__30 Source #
d_'8846''8660'Refl_84 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T_Equivalence_1714 Source #
d_sym_86 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_ReflClosure_30 → T_ReflClosure_30 Source #
du_sym_86 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_ReflClosure_30 → T_ReflClosure_30 Source #
d_trans_94 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_ReflClosure_30 → T_ReflClosure_30 → T_ReflClosure_30 Source #
du_trans_94 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_ReflClosure_30 → T_ReflClosure_30 → T_ReflClosure_30 Source #
d_antisym_114 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny → T_ReflClosure_30 → T_ReflClosure_30 → AgdaAny Source #
du_antisym_114 ∷ (AgdaAny → AgdaAny) → AgdaAny → T_ReflClosure_30 → T_ReflClosure_30 → AgdaAny Source #
d_total_140 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Tri_158) → AgdaAny → AgdaAny → T__'8846'__30 Source #
du_total_140 ∷ (AgdaAny → AgdaAny → T_Tri_158) → AgdaAny → AgdaAny → T__'8846'__30 Source #
d_dec_174 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_Dec_20 Source #
du_dec_174 ∷ (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_Dec_20 Source #
d_decidable_184 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Tri_158) → AgdaAny → AgdaAny → T_Dec_20 Source #
d_'46'extendedlambda0_220 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Tri_158) → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → (T__'8801'__12 → T_Irrelevant_20) → AgdaAny → T_ReflClosure_30 → T_Irrelevant_20 Source #
d_resp'737'_226 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_ReflClosure_30 → AgdaAny → AgdaAny Source #
du_resp'737'_226 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_ReflClosure_30 → AgdaAny → AgdaAny Source #
d_resp'691'_234 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_ReflClosure_30 → AgdaAny → AgdaAny Source #
du_resp'691'_234 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_ReflClosure_30 → AgdaAny → AgdaAny Source #
d_resp_250 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_ReflClosure_30 → AgdaAny → AgdaAny Source #
du_resp_250 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_ReflClosure_30 → AgdaAny → AgdaAny Source #
d_resp'8322'_270 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #
d__'126''7506'__282 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → () Source #
d_isPreorder_284 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsPreorder_70 Source #
du_isPreorder_284 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsPreorder_70 Source #
d_'46'extendedlambda0_288 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__'8801'__12 → T_ReflClosure_30 Source #
d_isPartialOrder_290 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_290 → T_IsPartialOrder_174 Source #
d_isDecPartialOrder_326 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_336 → T_IsDecPartialOrder_224 Source #
d_isTotalOrder_374 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_534 → T_IsTotalOrder_404 Source #
d_isDecTotalOrder_428 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_534 → T_IsDecTotalOrder_460 Source #