'the' function for inline type annotations
commit5501396beabf4099ee39824f756305bedf9343a6
authorBenjamin Saunders <besaunde@sfu.ca>
dateWed 28 Nov 2012, 14:59 (14 years ago)
parentf9e0605
lib/Builtins.idr+3
@@ -40,6 +40,9 @@ namespace Builtins {
4040id : a -> a
4141id x = x
4242
43+the : (A : Set) -> A -> A
44+the _ = id
45+
4346const : a -> b -> a
4447const x _ = x
4548