- 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 (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 a, DecEq b) => DecEq (a, b)
- DecEq a => DecEq (List a)
- DecEq a => DecEq (List1 a)
- DecEq Int
- 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- decEqContraIsNo : {auto conArg : DecEq a} -> Not (x = y) -> DPair (x = y -> Void) (\p => decEq x y = No p)
If you have a proof of inequality, you're sure that `decEq` would give a `No`.
Totality: total- decEqSelfIsYes : {auto conArg : DecEq a} -> decEq x x = Yes Refl
Everything is decidably equal to itself
Totality: total- negEqSym : Not (a = b) -> Not (b = a)
The negation of equality is symmetric (follows from symmetry of equality)
Totality: total