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:

All (DecEq . p) xs => DecEq (All p xs)

DecEq (Elem x xs)

DecEq (Elem x sx)

DecEq (Elem x xs)

DecEq (Elem x xs)

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 a => DecEq (Vect n a)

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:2599} : DecEq a} -> decEq x x = Yes Refl

  Everything is decidably equal to itself

Totality: total
Visibility: export

decEqContraIsNo : {auto {conArg:2663} : 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