- 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
- data Given : Dec a -> Type
- Totality: total
Constructor: - Always : Given (Yes x)
- 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- data IsYes : Dec a -> Type
Proof that some `Dec` is actually `Yes`
Totality: total
Constructor: - ItIsYes : IsYes (Yes prf)
- decide : Decidable k ts p => IsDecidable k ts p
- Totality: total
- isItYes : (v : Dec a) -> Dec (IsYes v)
Decide whether a 'Dec' is 'Yes'
Totality: total- isNo : Dec a -> Bool
- Totality: total
- isYes : Dec a -> Bool
- Totality: total