interface DecEq : Type -> Type
Decision procedures for propositional equality
Parameters: t
Methods:
decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
Decide whether two elements of `t` are propositionally equal
Implementations:
DecEq Namespace
DecEq UserName
DecEq Name
DecEq (Elem x xs)
DecEq (Elem x xs)
DecEq (Elem x sx)
DecEq a => DecEq (Vect n a)
DecEq ()
DecEq Bool
DecEq Nat
DecEq t => DecEq (Maybe t)
(DecEq t, DecEq s) => DecEq (Either t s)
DecEq t => DecEq s => DecEq (These t s)
(DecEq a, DecEq b) => DecEq (a, b)
DecEq a => DecEq (List a)
DecEq a => DecEq (List1 a)
DecEq a => DecEq (SnocList a)
DecEq Int
DecEq Bits8
DecEq Bits16
DecEq Bits32
DecEq Bits64
DecEq Int8
DecEq Int16
DecEq Int32
DecEq Int64
DecEq Char
DecEq Integer
DecEq String
DecEq (Fin n)
decEq : DecEq t => (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
Decide whether two elements of `t` are propositionally equal
Totality: total
Visibility: public exportnegEqSym : Not (a = b) -> Not (b = a)
The negation of equality is symmetric (follows from symmetry of equality)
Totality: total
Visibility: exportdecEqSelfIsYes : {auto {conArg:2621} : DecEq a} -> decEq x x = Yes Refl
Everything is decidably equal to itself
Totality: total
Visibility: exportdecEqContraIsNo : {auto {conArg:2685} : DecEq a} -> Not (x = y) -> (p : x = y -> Void ** decEq x y = No p)
If you have a proof of inequality, you're sure that `decEq` would give a `No`.
Totality: total
Visibility: exportdecEqCong : {auto 0 _ : Injective f} -> Dec (x = y) -> Dec (f x = f y)
- Totality: total
Visibility: public export decEqInj : {auto 0 _ : Injective f} -> Dec (f x = f y) -> Dec (x = y)
- Totality: total
Visibility: public export decEqCong2 : {auto 0 _ : Biinjective f} -> Dec (x = y) -> Lazy (Dec (v = w)) -> Dec (f x v = f y w)
- Totality: total
Visibility: public export