git.iko.soy/Idris-dev
on master help sign in
Uncommented the stuff in Decidable to see what happens.
956f888Timo Petteri Sinnemäki
libs/base/Decidable/Decidable.idr−2
compare with master
unifiedsplit
@@ -6,7 +6,6 @@ module Decidable.Decidable
6-- Typeclass for decidable n-ary Relations
6-- Typeclass for decidable n-ary Relations
7--------------------------------------------------------------------------------
7--------------------------------------------------------------------------------
8
8
9−{-
10This can't work yet! The class parameters must appear in the method type
9This can't work yet! The class parameters must appear in the method type
11signatures otherwise when defining the instances class resolution doesn't
10signatures otherwise when defining the instances class resolution doesn't
12have any clues...
11have any clues...
@@ -21,4 +20,3 @@ using (t : Type)
21using (P : Type, p : P)
20using (P : Type, p : P)
22 data Given : Dec P -> Type where
21 data Given : Dec P -> Type where
23 always : Given (Yes p)
22 always : Given (Yes p)
24−-}
libs/base/Decidable/Order.idr−3
@@ -2,7 +2,6 @@ module Decidable.Order
2
2
3%access public
3%access public
4
4
5−{-
6Doesn't work yet, see note in Decidable.idr
5Doesn't work yet, see note in Decidable.idr
7
6
8import Decidable.Decidable
7import Decidable.Decidable
@@ -83,5 +82,3 @@ instance Decidable NatLTE where
83lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
82lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
84lte m n = decide {p = NatLTE} m n
83lte m n = decide {p = NatLTE} m n
85
84
86−-}
87−