| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
Documentation
d_trans'45'refl'691'_24 ∷ T_Level_18 → () → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_trans'45'assoc_40 ∷ T_Level_18 → () → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #
d_trans'45'sym'737'_48 ∷ T_Level_18 → () → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_trans'45'sym'691'_56 ∷ T_Level_18 → () → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_trans'45'injective'737'_70 ∷ T_Level_18 → () → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #
d_trans'45'injective'691'_84 ∷ T_Level_18 → () → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #
d_cong'45'id_94 ∷ T_Level_18 → () → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_cong'45''8728'_106 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → AgdaAny → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T__'8801'__12 → T__'8801'__12 Source #
d_trans'45'cong_120 ∷ T_Level_18 → () → T_Level_18 → () → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny) → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #
d_cong'8322''45'refl'737'_134 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_cong'8322''45'refl'691'_148 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_subst'45'injective_170 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_subst'45'subst_182 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → AgdaAny → T__'8801'__12 Source #
d_subst'45'subst'45'sym_188 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → T__'8801'__12 Source #
d_subst'45'sym'45'subst_194 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → T__'8801'__12 Source #
d_subst'45''8728'_208 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → AgdaAny → AgdaAny → (AgdaAny → ()) → (AgdaAny → AgdaAny) → T__'8801'__12 → AgdaAny → T__'8801'__12 Source #
d_subst'45'application_240 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T__'8801'__12 → T__'8801'__12 Source #
d_isDecEquivalence_244 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_32) → T_IsDecEquivalence_44 Source #
d_isPreorder_248 ∷ T_Level_18 → () → T_IsPreorder_70 Source #
d_setoid_250 ∷ T_Level_18 → () → T_Setoid_44 Source #
d_decSetoid_254 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_32) → T_DecSetoid_84 Source #
du_decSetoid_254 ∷ (AgdaAny → AgdaAny → T_Dec_32) → T_DecSetoid_84 Source #
d_preorder_258 ∷ T_Level_18 → () → T_Preorder_132 Source #