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