Idris2Doc : Decidable.Equality.Core

Decidable.Equality.Core

Definitions

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)
DecEq (Elemxxs)
DecEq (Elemxxs)
DecEq ()
DecEqBool
DecEqNat
DecEqt=>DecEq (Maybet)
(DecEqt, DecEqs) =>DecEq (Eitherts)
DecEqt=>DecEqs=>DecEq (Thesets)
(DecEqa, DecEqb) =>DecEq (a, b)
DecEqa=>DecEq (Lista)
DecEqa=>DecEq (List1a)
DecEqa=>DecEq (SnocLista)
DecEqInt
DecEqBits8
DecEqBits16
DecEqBits32
DecEqBits64
DecEqInt8
DecEqInt16
DecEqInt32
DecEqInt64
DecEqChar
DecEqInteger
DecEqString
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
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:2618} : DecEqa} ->decEqxx=YesRefl
  Everything is decidably equal to itself

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

Totality: total
Visibility: export
decEqCong : {auto0_ : Injectivef} ->Dec (x=y) ->Dec (fx=fy)
Totality: total
Visibility: public export
decEqInj : {auto0_ : Injectivef} ->Dec (fx=fy) ->Dec (x=y)
Totality: total
Visibility: public export
decEqCong2 : {auto0_ : Biinjectivef} ->Dec (x=y) -> Lazy (Dec (v=w)) ->Dec (fxv=fyw)
Totality: total
Visibility: public export