Decidable.Equality.Core

Definitions

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 export

negEqSym : Not (a = b) -> Not (b = a)

  The negation of equality is symmetric (follows from symmetry of equality)

Totality: total
Visibility: export

decEqSelfIsYes : {auto {conArg:2621} : DecEq a} -> decEq x x = Yes Refl

  Everything is decidably equal to itself

Totality: total
Visibility: export

decEqContraIsNo : {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: export

decEqCong : {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