@@ -1,17 +1,21 @@
11module Decidable.Decidable
22
3+import Data.Rel
4+
35%access public
46
57--------------------------------------------------------------------------------
68-- Typeclass for decidable n-ary Relations
79--------------------------------------------------------------------------------
810
9−using (t : Type)
10− class Rel (p : t) where
11− total liftRel : (Type -> Type) -> Type
11+-- Note: Instance resolution for Decidable is likely to not work in the REPL
12+-- at the moment.
13+class Decidable (ts : Vect k Type) (p : Rel ts) where
14+ total decide : liftRel ts p Dec
1215
13− class (Rel p) => Decidable (p : t) where
14− total decide : liftRel {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}
1519
1620using (P : Type, p : P)
1721 data Given : Dec P -> Type where