git.iko.soy/Idris-dev
on 7d42ba2 help sign in
Idris-dev/libs/base/Decidable/Decidable.idr
23 lines 711 B history raw
1module Decidable.Decidable
3import Data.Rel
4import Data.Fun
6%access public
8--------------------------------------------------------------------------------
9-- Typeclass for decidable n-ary Relations
10--------------------------------------------------------------------------------
12-- Note: Instance resolution for Decidable is likely to not work in the REPL
13-- at the moment.
14class Decidable (ts : Vect k Type) (p : Rel ts) where
15 total decide : liftRel ts p Dec
17-- 'No such variable {k506}'
18--decision : Decidable ts p => (ts : Vect k Type) -> (p : Rel ts) -> liftRel ts p Dec
19--decision ts p = decide {ts} {p}
21using (a : Type, x : a)
22 data Given : Dec a -> Type where
23 Always : Given (Yes x)