| Safe Haskell | None |
|---|
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive
Documentation
d_ReflClosure_30 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #
data T_ReflClosure_30 Source #
Constructors
| C_refl_36 | |
| C_'91'_'93'_44 AgdaAny |
d_map_52 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> (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_14 -> () -> T_Level_14 -> (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_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T_ReflClosure_30 Source #
d_'91''93''45'injective_84 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 Source #
d_Refl_96 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> () Source #