Added always/Given as a non boolean equivalent for oh/so
commitc1d200d01bc5166b2cb6c35413ebe3ce1c46fdb4
authorJan Bessai <Jan.Bessai@tu-dortmund.de>
dateSun 14 Apr 2013, 19:02 (14 years ago)
parent75e5a39
lib/Decidable/Decidable.idr+5
@@ -12,3 +12,8 @@ using (t : Type)
1212
1313 class (Rel p) => Decidable (p : t) where
1414 total decide : liftRel Dec
15+
16+using (P : Type, p : P)
17+ data Given : Dec P -> Type where
18+ always : Given (Yes p)
19+