Idris2Doc : Decidable.Equality.Core

Decidable.Equality.Core

interfaceDecEq : 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 (Elemxxs)
DecEq (Elemxsx)
DecEqa => DecEq (Vectna)
DecEq ()
DecEqBool
DecEqNat
DecEqt => DecEq (Maybet)
(DecEqt, DecEqs) => DecEq (Eitherts)
(DecEqa, DecEqb) => DecEq (a, b)
DecEqa => DecEq (Lista)
DecEqa => DecEq (List1a)
DecEqInt
DecEqChar
DecEqInteger
DecEqString
DecEq (Finn)
decEq : DecEqt => (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
  Decide whether two elements of `t` are propositionally equal

Totality: total
decEqContraIsNo : {autoconArg : DecEqa} -> Not (x = y) -> DPair (x = y -> Void) (\p => decEqxy = Nop)
  If you have a proof of inequality, you're sure that `decEq` would give a `No`.

Totality: total
decEqSelfIsYes : {autoconArg : DecEqa} -> decEqxx = YesRefl
  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