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