Decidable.Equality.Eq

A form of decidable equality compatible with Eq

Definitions

data Decides : Bool -> Type -> Type

  Compatibility between a boolean and a proposition

Totality: total
Visibility: public export
Constructors:

Yes : p -> Decides True p

No : (p -> Void) -> Decides False p

interface EqIsDec : Type -> Type

  Decidable equality compatible with an Eq instance

Parameters: x
Constraints: Eq x
Methods:

eqDecides : (a : x) -> (b : x) -> Decides (a == b) (a = b)

Implementations:

EqIsDec ()

EqIsDec Bool

EqIsDec Nat

(EqIsDec a, EqIsDec b) => EqIsDec (Either a b)

(EqIsDec a, EqIsDec b) => EqIsDec (a, b)

EqIsDec a => EqIsDec (List a)

eqDecides : {auto __con : EqIsDec x} -> (a : x) -> (b : x) -> Decides (a == b) (a = b)

Visibility: public export

decidesToDec : Decides t p -> Dec p

Visibility: public export

eqPrec : S l = S r -> l = r

Visibility: public export

neSucc : (l = r -> Void) -> S l = S r -> Void

Visibility: public export

decSucc : Decides (m == n) (m = n) -> Decides (S m == S n) (S m = S n)

Visibility: public export