git.iko.soy/Idris-dev
on master help sign in
Uncommented the stuff in Decidable to see what happens.
commit956f888b16fb8d16289e4ff22c59f8e3fd73d1d4 authorTimo Petteri Sinnemäki <timo.sinnemaki@helsinki.fi> dateFri 17 Jan 2014, 19:27 (13 years ago) parent70ee9ef
2 files changed−5
compare with master
unifiedsplit
libs/base/Decidable/Decidable.idr−2 libs/base/Decidable/Order.idr−3
libs/base/Decidable/Decidable.idr−2
@@ -6,7 +6,6 @@ module Decidable.Decidable
66-- Typeclass for decidable n-ary Relations
77--------------------------------------------------------------------------------
88
9−{-
109This can't work yet! The class parameters must appear in the method type
1110signatures otherwise when defining the instances class resolution doesn't
1211have any clues...
@@ -21,4 +20,3 @@ using (t : Type)
2120using (P : Type, p : P)
2221 data Given : Dec P -> Type where
2322 always : Given (Yes p)
24−-}
libs/base/Decidable/Order.idr−3
@@ -2,7 +2,6 @@ module Decidable.Order
22
33%access public
44
5−{-
65Doesn't work yet, see note in Decidable.idr
76
87import Decidable.Decidable
@@ -83,5 +82,3 @@ instance Decidable NatLTE where
8382lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
8483lte m n = decide {p = NatLTE} m n
8584
86−-}
87−