Decidable.idr

module Decidable.Decidable

%access public

--------------------------------------------------------------------------------
-- Typeclass for decidable n-ary Relations
--------------------------------------------------------------------------------

{-
This can't work yet! The class parameters must appear in the method type
signatures otherwise when defining the instances class resolution doesn't
have any clues...

using (t : Type)
  class Rel (p : t) where
    total liftRel : (Type -> Type) -> Type

  class (Rel p) => Decidable (p : t) where
    total decide : liftRel Dec

using (P : Type, p : P)
  data Given : Dec P -> Type where
    always : Given (Yes p)
-}