on master help sign in
Add Not definition
019aea7Benjamin Saunders
lib/Builtins.idr+3
@@ -44,6 +44,9 @@ really_believe_me x = prim__believe_me _ _ x
44
44
45namespace Builtins {
45namespace Builtins {
46
46
47+Not : Type -> Type
48+Not a = a -> _|_
49+
47id : a -> a
50id : a -> a
48id x = x
51id x = x
49
52