git.iko.soy/Idris-dev
on master help sign in
Explicit instance to liftRel apparently makes Decidable work.
commitd774fbda397295cc49ac122da9582d6c98ab1699 authorTimo Petteri Sinnemäki <timo.sinnemaki@helsinki.fi> dateFri 17 Jan 2014, 21:05 (13 years ago) parent956f888
2 files changed+6−8
compare with master
unifiedsplit
libs/base/Decidable/Decidable.idr+4−4 libs/base/Decidable/Order.idr+2−4
libs/base/Decidable/Decidable.idr+4−4
@@ -6,16 +6,16 @@ module Decidable.Decidable
66-- Typeclass for decidable n-ary Relations
77--------------------------------------------------------------------------------
88
9−This can't work yet! The class parameters must appear in the method type
10−signatures otherwise when defining the instances class resolution doesn't
11−have any clues...
9+--This can't work yet! The class parameters must appear in the method type
10+--signatures otherwise when defining the instances class resolution doesn't
11+--have any clues...
1212
1313using (t : Type)
1414 class Rel (p : t) where
1515 total liftRel : (Type -> Type) -> Type
1616
1717 class (Rel p) => Decidable (p : t) where
18− total decide : liftRel Dec
18+ total decide : liftRel {p=p} Dec
1919
2020using (P : Type, p : P)
2121 data Given : Dec P -> Type where
libs/base/Decidable/Order.idr+2−4
@@ -1,12 +1,10 @@
11module Decidable.Order
22
3−%access public
4−
5−Doesn't work yet, see note in Decidable.idr
6−
73import Decidable.Decidable
84import Decidable.Equality
95
6+%access public
7+
108--------------------------------------------------------------------------------
119-- Utility Lemmas
1210--------------------------------------------------------------------------------