Idris2Doc : Decidable.Equality.Core

# Decidable.Equality.Core

DecEq : Type -> Type
Decision procedures for propositional equality
Parameters: t
Methods:
decEq : (x1 : t) -> (x2 : t) -> Dec _
Decide whether two elements of `t` are propositionally equal

Implementations:
DecEq (Elemxxs)
DecEqUnit
DecEqBool
DecEqNat
DecEqt => DecEq (Maybet)
(DecEqt, DecEqs) => DecEq (Eitherts)
(DecEqa, DecEqb) => DecEq (a, b)
DecEqa => DecEq (Lista)
DecEqa => DecEq (List1a)
DecEq Int
DecEq Char
DecEq Integer
DecEq String
DecEqa => DecEq (Vectna)
DecEq (Finn)
decEq : DecEqt => (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
Decide whether two elements of `t` are propositionally equal
Totality: total
decEqContraIsNo : {auto {conArg:442} : 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 : {auto {conArg:390} : 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