| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive
Documentation
d_ReflClosure_30 ∷ p → p → p → p → p → p → () Source #
data T_ReflClosure_30 Source #
Constructors
| C_refl_36 | |
| C_'91'_'93'_44 AgdaAny |
d_map_52 ∷ 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_map_52 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_ReflClosure_30 → T_ReflClosure_30 Source #
d_drop'45'refl_62 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_ReflClosure_30 → AgdaAny Source #
du_drop'45'refl_62 ∷ (AgdaAny → AgdaAny) → AgdaAny → T_ReflClosure_30 → AgdaAny Source #
d_reflexive_72 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T__'8801'__12 → T_ReflClosure_30 Source #
d_'91''93''45'injective_84 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_Refl_96 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → () Source #