| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Definitions
Documentation
d_Reflexive_26 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #
d_Sym_32 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #
d_Symmetric_38 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #
d_Trans_42 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #
d_RightTrans_56 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #
d_LeftTrans_62 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #
d_TransFlip_68 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #
d_Transitive_82 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #
d_Antisym_86 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #
d_Antisymmetric_98 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #
d_Irreflexive_104 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #
d_Asymmetric_114 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #
d_Dense_122 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #
d_Connex_132 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #
d_Total_142 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #
Constructors
| C_tri'60'_172 AgdaAny | |
| C_tri'8776'_180 AgdaAny | |
| C_tri'62'_188 AgdaAny |
d_Trichotomous_190 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #
d__'62'__200 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → () Source #
d_Max_206 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → () Source #
d_Maximum_214 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → () Source #
d_Min_216 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → () Source #
d_Minimum_220 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → () Source #
d_Cotransitive_222 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #
d_Tight_232 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #
d_Monotonic'8321'_242 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → () Source #
d_Antitonic'8321'_250 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → () Source #
d_LeftMonotonic_254 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_RightMonotonic_266 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Monotonic'8322'_278 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_MonotonicAntitonic_288 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_AntitonicMonotonic_294 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Antitonic'8322'_298 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Adjoint_304 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #
d__'10230'_Respects__318 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #
d__Respects__330 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #
d__Respects'691'__336 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #
d__Respects'737'__346 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #
d__Respects'8322'__354 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #
d_Substitutive_362 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () Source #
d_Irrelevant_372 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #
d_Recomputable_380 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #
d_Stable_388 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #
d_WeaklyDecidable_396 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #
d_Decidable_404 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #
d_DecidableEquality_414 ∷ T_Level_18 → () → () Source #
d_Universal_418 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #
d_Empty_426 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #
d_NonEmpty_446 ∷ p → p → p → p → p → p → () Source #
data T_NonEmpty_446 Source #
Constructors
| C_nonEmpty_466 AgdaAny AgdaAny AgdaAny |