git.iko.soy/Idris-dev
on d79a445 help sign in
Idris-dev/lib/Decidable/Decidable.idr
19 lines 499 B history raw
1module Decidable.Decidable
3%access public
5--------------------------------------------------------------------------------
6-- Typeclass for decidable n-ary Relations
7--------------------------------------------------------------------------------
9using (t : Type)
10 class Rel (p : t) where
11 total liftRel : (Type -> Type) -> Type
13 class (Rel p) => Decidable (p : t) where
14 total decide : liftRel Dec
16using (P : Type, p : P)
17 data Given : Dec P -> Type where
18 always : Given (Yes p)