git.iko.soy/Idris-dev
on master help sign in
Added always/Given as a non boolean equivalent for oh/so
c1d200dJan Bessai
lib/Decidable/Decidable.idr+5
compare with master
unifiedsplit
@@ -12,3 +12,8 @@ using (t : Type)
12
12
13 class (Rel p) => Decidable (p : t) where
13 class (Rel p) => Decidable (p : t) where
14 total decide : liftRel Dec
14 total decide : liftRel Dec
15+
16+using (P : Type, p : P)
17+ data Given : Dec P -> Type where
18+ always : Given (Yes p)
19+