| 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 #
d_'58''8594''45'to'45'Π_38 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> T_IndexedSetoid_18 -> (AgdaAny -> AgdaAny) -> T_Func_42 #
du_'58''8594''45'to'45'Π_38 :: T_IndexedSetoid_18 -> (AgdaAny -> AgdaAny) -> T_Func_42 #
d_'46'extendedlambda0_44 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> T_IndexedSetoid_18 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #
du_'46'extendedlambda0_44 :: T_IndexedSetoid_18 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #
d_'8594''45'to'45''10230'_50 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Func_42 #
du_'8594''45'to'45''10230'_50 :: T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Func_42 #
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 #
d_cong'45''8801'id_84 :: T_Level_18 -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> T__'8801'__12) -> T__'8801'__12 #
d_fx'8801'x_96 :: T_Level_18 -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> T__'8801'__12) -> T__'8801'__12 #
d_f'178'x'8801'x_98 :: T_Level_18 -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> T__'8801'__12) -> T__'8801'__12 #
d_'8801''45''8799''45'identity_118 :: T_Level_18 -> () -> (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #
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 #
d_Reveal_'183'_is__142 :: p -> p -> p -> p -> p -> p -> p -> () #
data T_Reveal_'183'_is__142 #
Constructors
| C_'91'_'93'_158 |
d_inspect_170 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Reveal_'183'_is__142 #
d_isPropositional_176 :: T_Level_18 -> () -> () #