| Safe Haskell | None |
|---|
MAlonzo.Code.Relation.Binary.Definitions
Documentation
d_Reflexive_26 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d_Sym_32 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d_Symmetric_38 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d_Trans_42 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d_TransFlip_56 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d_Transitive_70 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d_Antisym_74 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d_Antisymmetric_86 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d_Irreflexive_92 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d_Asymmetric_102 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d_Connex_110 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d_Total_120 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> () Source #
Constructors
| C_tri'60'_150 AgdaAny | |
| C_tri'8776'_158 AgdaAny | |
| C_tri'62'_166 AgdaAny |
d_Trichotomous_168 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d__'62'__178 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> () Source #
d_Max_184 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> () Source #
d_Maximum_192 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> () Source #
d_Min_194 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> () Source #
d_Minimum_198 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> () Source #
d__'10230'_Respects__200 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d__Respects__212 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d__Respects'691'__218 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d__Respects'737'__228 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d__Respects'8322'__236 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d_Substitutive_244 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> () Source #
d_Decidable_254 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d_WeaklyDecidable_262 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d_DecidableEquality_272 :: T_Level_14 -> () -> () Source #
d_Irrelevant_276 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d_Recomputable_288 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d_Universal_296 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> () Source #
d_NonEmpty_316 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #
data T_NonEmpty_316 Source #
Constructors
| C_nonEmpty_336 AgdaAny AgdaAny AgdaAny |
d_x_330 :: T_NonEmpty_316 -> AgdaAny Source #
d_y_332 :: T_NonEmpty_316 -> AgdaAny Source #
d_proof_334 :: T_NonEmpty_316 -> AgdaAny Source #
d_Conn_338 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () Source #