on master help sign in
Add Not definition
commit019aea7c1dece8368fd1b945721533ac5c82cfd3 authorBenjamin Saunders <besaunde@sfu.ca> dateSat 27 Apr 2013, 17:01 (14 years ago) parentd1cb783
1 file changed+3
lib/Builtins.idr+3
lib/Builtins.idr+3
@@ -44,6 +44,9 @@ really_believe_me x = prim__believe_me _ _ x
4444
4545namespace Builtins {
4646
47+Not : Type -> Type
48+Not a = a -> _|_
49+
4750id : a -> a
4851id x = x
4952