git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/libs/base/Decidable/Decidable.idr
22 lines 695 B history raw
1module Decidable.Decidable
3import Data.Rel
5%access public
7--------------------------------------------------------------------------------
8-- Typeclass for decidable n-ary Relations
9--------------------------------------------------------------------------------
11-- Note: Instance resolution for Decidable is likely to not work in the REPL
12-- at the moment.
13class Decidable (ts : Vect k Type) (p : Rel ts) where
14 total decide : liftRel ts p Dec
16-- 'No such variable {k506}'
17--decision : Decidable ts p => (ts : Vect k Type) -> (p : Rel ts) -> liftRel ts p Dec
18--decision ts p = decide {ts} {p}
20using (P : Type, p : P)
21 data Given : Dec P -> Type where
22 always : Given (Yes p)