| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.PropositionalEquality.Core
Documentation
d__'8802'__22 ∷ T_Level_18 → () → AgdaAny → AgdaAny → () Source #
d__'8791'__32 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #
d_cong_54 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_cong'8242'_62 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → T__'8801'__12 Source #
d_icong_70 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_icong'8242'_76 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → T__'8801'__12 Source #
d_cong'8322'_88 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #
d_cong'45'app_104 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T__'8801'__12 → AgdaAny → T__'8801'__12 Source #
d_sym_108 ∷ T_Level_18 → () → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_trans_110 ∷ T_Level_18 → () → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #
d_subst_114 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → AgdaAny Source #
d_subst'8322'_130 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → AgdaAny → AgdaAny Source #
d_resp_136 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → AgdaAny Source #
du_resp_136 ∷ AgdaAny → AgdaAny Source #
d_resp'737'_144 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → AgdaAny Source #
d_resp'691'_152 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → AgdaAny Source #
d_resp'8322'_160 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Σ_14 Source #
d_'8802''45'sym_164 ∷ T_Level_18 → () → AgdaAny → AgdaAny → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 → T_Irrelevant_20 Source #