on master help sign in
Remove comments in Decidable.Decidable
commitec4ccc9473914fd3435dd54e4619eed48e141e6b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 18 Jan 2014, 19:32 (13 years ago) parente4d99ee
1 file changed+1−5
libs/base/Decidable/Decidable.idr+1−5
libs/base/Decidable/Decidable.idr+1−5
@@ -6,16 +6,12 @@ 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...
12−
139using (t : Type)
1410 class Rel (p : t) where
1511 total liftRel : (Type -> Type) -> Type
1612
1713 class (Rel p) => Decidable (p : t) where
18− total decide : liftRel {p=p} Dec
14+ total decide : liftRel {p} Dec
1915
2016using (P : Type, p : P)
2117 data Given : Dec P -> Type where