| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Unary.Properties
Documentation
d_'8709''63'_22 ∷ T_Level_18 → () → AgdaAny → T_Dec_20 Source #
d_'8709''45'Empty_24 ∷ T_Level_18 → () → AgdaAny → T_Irrelevant_20 → T_Irrelevant_20 Source #
d_'8705''8709''45'Universal_28 ∷ T_Level_18 → () → AgdaAny → T_Irrelevant_20 → T_Irrelevant_20 Source #
d_U'63'_34 ∷ T_Level_18 → () → AgdaAny → T_Dec_20 Source #
d_U'45'Universal_36 ∷ T_Level_18 → () → AgdaAny → T_'8868'_6 Source #
d_'8705'U'45'Empty_40 ∷ T_Level_18 → () → AgdaAny → (T_'8868'_6 → T_Irrelevant_20) → T_Irrelevant_20 Source #
d_'8709''45''8838'_48 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → T_Irrelevant_20 → AgdaAny Source #
d_'8838''45'U_54 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → AgdaAny → T_'8868'_6 Source #
d_'8838''45'refl_58 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny Source #
d_'8838''45'reflexive_62 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8838''45'trans_68 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_'8838''45'trans_68 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_'8838''45'antisym_76 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #
du_'8838''45'antisym_76 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8838''45'min_78 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → T_Irrelevant_20 → AgdaAny Source #
du_'8838''45'min_78 ∷ (AgdaAny → ()) → AgdaAny → T_Irrelevant_20 → AgdaAny Source #
d_'8838''45'max_80 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → AgdaAny → T_'8868'_6 Source #
du_'8838''45'max_80 ∷ (AgdaAny → ()) → AgdaAny → AgdaAny → T_'8868'_6 Source #
d_'8834''8658''8838'_82 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8834''45'trans_84 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'8834''45''8838''45'trans_100 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8838''45''8834''45'trans_114 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 Source #
d_'8834''45'resp'691''45''8784'_128 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'8834''45'resp'737''45''8784'_134 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'8834''45'resp'45''8784'_140 ∷ T_Level_18 → () → T_Level_18 → T_Σ_14 Source #
d_'8834''45'irrefl_142 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Irrelevant_20 Source #
d_'8834''45'antisym_148 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'8834''45'asym_154 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Irrelevant_20 Source #
d_'8709''45''8838''8242'_160 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → T_Irrelevant_20 → AgdaAny Source #
d_'8838''8242''45'U_164 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → AgdaAny → T_'8868'_6 Source #
d_'8838''8242''45'refl_166 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny Source #
d_'8838''8242''45'reflexive_172 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8838''8242''45'trans_178 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_'8838''8242''45'trans_178 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_'8838''8242''45'antisym_188 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #
du_'8838''8242''45'antisym_188 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8838''8242''45'min_190 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → T_Irrelevant_20 → AgdaAny Source #
du_'8838''8242''45'min_190 ∷ T_Level_18 → T_Level_18 → (AgdaAny → ()) → AgdaAny → T_Irrelevant_20 → AgdaAny Source #
d_'8838''8242''45'max_192 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → AgdaAny → T_'8868'_6 Source #
du_'8838''8242''45'max_192 ∷ (AgdaAny → ()) → AgdaAny → AgdaAny → T_'8868'_6 Source #
d_'8834''8242''8658''8838''8242'_194 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8834''8242''45'trans_196 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'8834''8242''45''8838''8242''45'trans_208 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #
du_'8834''8242''45''8838''8242''45'trans_208 ∷ T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8838''8242''45''8834''8242''45'trans_218 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 Source #
du_'8838''8242''45''8834''8242''45'trans_218 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 Source #
d_'8834''8242''45'resp'691''45''8784''8242'_228 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'8834''8242''45'resp'737''45''8784''8242'_234 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'8834''8242''45'irrefl_242 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Irrelevant_20 Source #
d_'8834''8242''45'antisym_248 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'8838''8658''8838''8242'_254 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_'8838''8658''8838''8242'_254 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_'8838''8242''8658''8838'_260 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_'8838''8242''8658''8838'_260 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_'8834''8658''8834''8242'_266 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #
d_'8834''8242''8658''8834'_270 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #
d_'8784''45'refl_274 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Σ_14 Source #
d_'8784''45'sym_276 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #
d_'8784''45'trans_278 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'8784''8242''45'refl_292 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Σ_14 Source #
d_'8784''8242''45'sym_298 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #
d_'8784''8242''45'trans_300 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'8784''8658''8784''8242'_318 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #
d_'8784''8242''8658''8784'_320 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #
d_'8812''45'symmetric_322 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #
d_'8869''45'symmetric_324 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → T_Σ_14 → T_Irrelevant_20) → AgdaAny → T_Σ_14 → T_Irrelevant_20 Source #
d_'8812''45'sym_328 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #
d_'8869''45'sym_330 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → T_Σ_14 → T_Irrelevant_20) → AgdaAny → T_Σ_14 → T_Irrelevant_20 Source #
d_'8812''8658''172''8869'_332 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → (AgdaAny → T_Σ_14 → T_Irrelevant_20) → T_Irrelevant_20 Source #
d_'8869''8658''172''8812'_338 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → T_Σ_14 → T_Irrelevant_20) → T_Σ_14 → T_Irrelevant_20 Source #
d_map_346 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → (AgdaAny → T_Dec_20) → AgdaAny → T_Dec_20 Source #
d_'8705''63'_358 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → AgdaAny → T_Dec_20 Source #
d__'8746''63'__368 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → T_Dec_20) → AgdaAny → T_Dec_20 Source #
d__'8745''63'__380 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → T_Dec_20) → AgdaAny → T_Dec_20 Source #
d__'215''63'__392 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → T_Dec_20) → T_Σ_14 → T_Dec_20 Source #
d__'8857''63'__406 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → T_Dec_20) → T_Σ_14 → T_Dec_20 Source #
d__'8846''63'__420 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → T_Dec_20) → T__'8846'__30 → T_Dec_20 Source #
du__'8846''63'__420 ∷ (AgdaAny → T_Dec_20) → (AgdaAny → T_Dec_20) → T__'8846'__30 → T_Dec_20 Source #
d__'126''63'_436 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (T_Σ_14 → ()) → (T_Σ_14 → T_Dec_20) → T_Σ_14 → T_Dec_20 Source #
d_does'45''8801'_446 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → T_Dec_20) → AgdaAny → T__'8801'__12 Source #
d_does'45''8784'_462 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → (AgdaAny → T_Dec_20) → (AgdaAny → T_Dec_20) → AgdaAny → T__'8801'__12 Source #
d_U'45'irrelevant_468 ∷ T_Level_18 → () → AgdaAny → T_'8868'_6 → T_'8868'_6 → T__'8801'__12 Source #
d_'8705''45'irrelevant_476 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → (AgdaAny → T_Irrelevant_20) → (AgdaAny → T_Irrelevant_20) → T__'8801'__12 Source #