| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Function.Injection
Documentation
d_Injective_16 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Π_16 → () Source #
d_Injection_88 ∷ p → p → p → p → p → p → () Source #
data T_Injection_88 Source #
d_injective_108 ∷ T_Injection_88 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_cong_114 ∷ T_Injection_88 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d__'8611'__120 ∷ T_Level_18 → T_Level_18 → () → () → () Source #
d_injection_140 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12) → T_Injection_88 Source #
du_injection_140 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12) → T_Injection_88 Source #