Idris2Doc : Decidable.Equality.Core

# 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