Idris2Doc : Decidable.Decidable

Decidable.Decidable

interfaceDecidable : (k : Nat) -> (ts : VectkType) -> FuntsType -> Type
  Interface for decidable n-ary Relations

Parameters: k, ts, p
Methods:
decide : IsDecidablektsp

Implementations:
Decidable2 [Nat, Nat] LTE
Decidable2 [Nat, Nat] LT
Decidable2 [Fink, Fink] FinLTE
dataGiven : Deca -> Type
Totality: total
Constructor: 
Always : Given (Yesx)
IsDecidable : (k : Nat) -> (ts : VectkType) -> Relts -> Type
  An n-ary relation is decidable if we can make a `Dec`
of its result type for each combination of inputs

Totality: total
dataIsYes : Deca -> Type
  Proof that some `Dec` is actually `Yes`

Totality: total
Constructor: 
ItIsYes : IsYes (Yesprf)
decide : Decidablektsp => IsDecidablektsp
Totality: total
isItYes : (v : Deca) -> Dec (IsYesv)
  Decide whether a 'Dec' is 'Yes'

Totality: total
isNo : Deca -> Bool
Totality: total
isYes : Deca -> Bool
Totality: total