git.iko.soy/Idris-dev
on master help sign in
Explicit instance to liftRel apparently makes Decidable work.
d774fbdTimo Petteri Sinnemäki
libs/base/Decidable/Decidable.idr+4−4
compare with master
unifiedsplit
@@ -6,16 +6,16 @@ module Decidable.Decidable
6-- Typeclass for decidable n-ary Relations
6-- Typeclass for decidable n-ary Relations
7--------------------------------------------------------------------------------
7--------------------------------------------------------------------------------
8
8
9−This can't work yet! The class parameters must appear in the method type
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
10+--signatures otherwise when defining the instances class resolution doesn't
11−have any clues...
11+--have any clues...
12
12
13using (t : Type)
13using (t : Type)
14 class Rel (p : t) where
14 class Rel (p : t) where
15 total liftRel : (Type -> Type) -> Type
15 total liftRel : (Type -> Type) -> Type
16
16
17 class (Rel p) => Decidable (p : t) where
17 class (Rel p) => Decidable (p : t) where
18− total decide : liftRel Dec
18+ total decide : liftRel {p=p} Dec
19
19
20using (P : Type, p : P)
20using (P : Type, p : P)
21 data Given : Dec P -> Type where
21 data Given : Dec P -> Type where
libs/base/Decidable/Order.idr+2−4
@@ -1,12 +1,10 @@
1module Decidable.Order
1module Decidable.Order
2
2
3−%access public
4−
5−Doesn't work yet, see note in Decidable.idr
6−
7import Decidable.Decidable
3import Decidable.Decidable
8import Decidable.Equality
4import Decidable.Equality
9
5
6+%access public
7+
10--------------------------------------------------------------------------------
8--------------------------------------------------------------------------------
11-- Utility Lemmas
9-- Utility Lemmas
12--------------------------------------------------------------------------------
10--------------------------------------------------------------------------------