@@ -6,16 +6,12 @@ module Decidable.Decidable
6-- Typeclass for decidable n-ary Relations
6-- Typeclass for decidable n-ary Relations
7--------------------------------------------------------------------------------
7--------------------------------------------------------------------------------
9−--This can't work yet! The class parameters must appear in the method type
10−--signatures otherwise when defining the instances class resolution doesn't
13using (t : Type)
9using (t : Type)
14 class Rel (p : t) where
10 class Rel (p : t) where
15 total liftRel : (Type -> Type) -> Type
11 total liftRel : (Type -> Type) -> Type
17 class (Rel p) => Decidable (p : t) where
13 class (Rel p) => Decidable (p : t) where
18− total decide : liftRel {p=p} Dec
14+ total decide : liftRel {p} Dec
20using (P : Type, p : P)
16using (P : Type, p : P)
21 data Given : Dec P -> Type where
17 data Given : Dec P -> Type where