git.iko.soy/Idris-dev
on de0bcbd help sign in
Idris-dev/lib/Decidable/Decidable.idr
24 lines 670 B history raw
1module Decidable.Decidable
3%access public
5--------------------------------------------------------------------------------
6-- Typeclass for decidable n-ary Relations
7--------------------------------------------------------------------------------
9{-
10This can't work yet! The class parameters must appear in the method type
11signatures otherwise when defining the instances class resolution doesn't
12have any clues...
14using (t : Type)
15 class Rel (p : t) where
16 total liftRel : (Type -> Type) -> Type
18 class (Rel p) => Decidable (p : t) where
19 total decide : liftRel Dec
21using (P : Type, p : P)
22 data Given : Dec P -> Type where
23 always : Given (Yes p)
24-}