| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
Documentation
d_J_34 :: T_Level_18 -> T_Level_18 -> () -> AgdaAny -> (AgdaAny -> T__'8801'__12 -> ()) -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny #
d_dcong_54 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #
d_dcong'8322'_78 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #
d_dsubst'8322'_100 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 -> AgdaAny -> AgdaAny #
du_dsubst'8322'_100 :: AgdaAny -> AgdaAny #
d_ddcong'8322'_132 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #
d_trans'45'refl'691'_142 :: T_Level_18 -> () -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #
d_trans'45'assoc_158 :: T_Level_18 -> () -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #
d_trans'45'sym'737'_166 :: T_Level_18 -> () -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #
d_trans'45'sym'691'_174 :: T_Level_18 -> () -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #
d_trans'45'injective'737'_188 :: T_Level_18 -> () -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #
d_trans'45'injective'691'_202 :: T_Level_18 -> () -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #
d_cong'45'id_212 :: T_Level_18 -> () -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #
d_cong'45''8728'_224 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T__'8801'__12 -> T__'8801'__12 #
d_sym'45'cong_234 :: T_Level_18 -> () -> T_Level_18 -> () -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny) -> T__'8801'__12 -> T__'8801'__12 #
d_trans'45'cong_248 :: T_Level_18 -> () -> T_Level_18 -> () -> AgdaAny -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny) -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #
d_cong'8322''45'refl'737'_262 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #
d_cong'8322''45'refl'691'_276 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #
d_subst'45'injective_298 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #
d_subst'45'subst_310 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 -> AgdaAny -> T__'8801'__12 #
d_subst'45'subst'45'sym_316 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> T__'8801'__12 #
d_subst'45'sym'45'subst_322 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> T__'8801'__12 #
d_subst'45''8728'_336 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> AgdaAny -> AgdaAny -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T__'8801'__12 -> AgdaAny -> T__'8801'__12 #
d_subst'45'application'8242'_362 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T__'8801'__12 -> T__'8801'__12 #
d_subst'45'application_394 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T__'8801'__12 -> T__'8801'__12 #
d_isEquivalence_396 :: T_Level_18 -> () -> T_IsEquivalence_26 #
d_isDecEquivalence_398 :: T_Level_18 -> () -> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecEquivalence_44 #
du_isDecEquivalence_398 :: (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecEquivalence_44 #
d_setoid_402 :: T_Level_18 -> () -> T_Setoid_44 #
d_decSetoid_406 :: T_Level_18 -> () -> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecSetoid_84 #
du_decSetoid_406 :: (AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecSetoid_84 #
d_isPreorder_410 :: T_Level_18 -> () -> T_IsPreorder_70 #
d_isPartialOrder_412 :: T_Level_18 -> () -> T_IsPartialOrder_174 #
d_preorder_414 :: T_Level_18 -> () -> T_Preorder_132 #
d_poset_418 :: T_Level_18 -> () -> T_Poset_314 #
d_begin__430 :: T_Level_18 -> () -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #
d_step'45''8801'_434 :: T_Level_18 -> () -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #
d_step'45''8801''45''8739'_436 :: T_Level_18 -> () -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #
d_step'45''8801''45''10216'_438 :: T_Level_18 -> () -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #
d_step'45''8801''45''10217'_440 :: T_Level_18 -> () -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #
d_step'45''8801''728'_442 :: T_Level_18 -> () -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #
d__'8718'_446 :: T_Level_18 -> () -> AgdaAny -> T__'8801'__12 #