| 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_16 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_'8869'_4) → 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_136) → AgdaAny → AgdaAny → T__'8846'__30 Source #
du_total_140 ∷ (AgdaAny → AgdaAny → T_Tri_136) → AgdaAny → AgdaAny → T__'8846'__30 Source #
d_dec_174 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → T_Dec_32) → AgdaAny → AgdaAny → T_Dec_32 Source #
du_dec_174 ∷ (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → T_Dec_32) → AgdaAny → AgdaAny → T_Dec_32 Source #
d_decidable_184 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Tri_136) → AgdaAny → AgdaAny → T_Dec_32 Source #
d_'46'extendedlambda0_220 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Tri_136) → AgdaAny → AgdaAny → (AgdaAny → T_'8869'_4) → (T__'8801'__12 → T_'8869'_4) → AgdaAny → T_ReflClosure_30 → T_'8869'_4 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_266 → T_IsPartialOrder_162 Source #
d_isDecPartialOrder_328 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_314 → T_IsDecPartialOrder_206 Source #
d_isTotalOrder_378 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → T_IsTotalOrder_384 Source #
d_isDecTotalOrder_430 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → T_IsDecTotalOrder_434 Source #