| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.PropositionalEquality
Documentation
d__'8594''45'setoid__26 ∷ T_Level_18 → T_Level_18 → () → () → T_Setoid_44 Source #
d_'58''8594''45'to'45'Π_38 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → T_IndexedSetoid_18 → (AgdaAny → AgdaAny) → T_Func_42 Source #
d_'46'extendedlambda0_44 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → T_IndexedSetoid_18 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #
d_'8594''45'to'45''10230'_50 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → T_Setoid_44 → (AgdaAny → AgdaAny) → T_Func_42 Source #
d_naturality_66 ∷ T_Level_18 → () → T_Level_18 → () → AgdaAny → AgdaAny → T__'8801'__12 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T__'8801'__12 Source #
d_cong'45''8801'id_84 ∷ T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → T__'8801'__12) → T__'8801'__12 Source #
d_fx'8801'x_96 ∷ T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → T__'8801'__12) → T__'8801'__12 Source #
d_f'178'x'8801'x_98 ∷ T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → T__'8801'__12) → T__'8801'__12 Source #
d_'8801''45''8799''45'identity_118 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_'8802''45''8799''45'identity_124 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 Source #
d_Reveal_'183'_is__142 ∷ p → p → p → p → p → p → p → () Source #
data T_Reveal_'183'_is__142 Source #
Constructors
| C_'91'_'93'_158 |
d_inspect_170 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → T_Reveal_'183'_is__142 Source #
d_isPropositional_176 ∷ T_Level_18 → () → () Source #