Decidable.Decidable

Definitions

isNo : Dec a -> Bool

Totality: total
Visibility: public export

isYes : Dec a -> Bool

Totality: total
Visibility: public export

data IsYes : Dec a -> Type

  Proof that some `Dec` is actually `Yes`

Totality: total
Visibility: public export
Constructor: 

ItIsYes : IsYes (Yes prf)

Hint: 

Uninhabited (IsYes (No contra))

isItYes : (v : Dec a) -> Dec (IsYes v)

  Decide whether a 'Dec' is 'Yes'

Totality: total
Visibility: public export

IsDecidable : (k : Nat) -> (ts : Vect k Type) -> Rel ts -> Type

  An n-ary relation is decidable if we can make a `Dec`
  of its result type for each combination of inputs

Totality: total
Visibility: public export

interface Decidable : (k : Nat) -> (ts : Vect k Type) -> Fun ts Type -> Type

  Interface for decidable n-ary Relations

Parameters: k, ts, p
Methods:

decide : IsDecidable k ts p

Implementations:

Decidable 2 [Nat, Nat] LTE

Decidable 2 [Nat, Nat] LT

Decidable 2 [Fin k, Fin k] FinLTE

decide : Decidable k ts p => IsDecidable k ts p

Totality: total
Visibility: public export

decision : (ts : Vect k Type) -> (p : Rel ts) -> Decidable k ts p => liftRel ts p Dec

  Given a `Decidable` n-ary relation, provides a decision procedure for
  this relation.

Totality: total
Visibility: public export