| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive
Documentation
d_ReflClosure_30 :: p -> p -> p -> p -> p -> p -> () #
data T_ReflClosure_30 #
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 #
du_map_52 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30 #
d_drop'45'refl_62 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> AgdaAny #
du_drop'45'refl_62 :: (AgdaAny -> AgdaAny) -> AgdaAny -> T_ReflClosure_30 -> AgdaAny #
d_reflexive_72 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T_ReflClosure_30 #
d_'91''93''45'injective_84 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #
d_Refl_96 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> () #