Idris2Doc : Decidable.Decidable

Decidable.Decidable

Decidable : (k : Nat) -> (ts : Vectk Type) -> Funts Type -> Type
Interface for decidable n-ary Relations
Parameters: k, ts, p
Methods:
decide : IsDecidablektsp
total

Implementations:
Decidable 2 [Nat, Nat] LTE
Decidable 2 [Fink, Fink] FinLTE
Given : Deca -> Type
Totality: total
Constructor: 
Always : Given (Yesx)
IsDecidable : (k : Nat) -> (ts : Vectk Type) -> Relts -> Type
An n-ary relation is decidable if we can make a `Dec`
of its result type for each combination of inputs
IsYes : Deca -> Type
Proof that some `Dec` is actually `Yes`
Totality: total
Constructor: 
ItIsYes : IsYes (Yesprf)
decide : Decidablektsp => IsDecidablektsp
isItYes : (v : Deca) -> Dec (IsYesv)
Decide whether a 'Dec' is 'Yes'
isNo : Deca -> Bool
isYes : Deca -> Bool