Merge pull request #108 from bitlisp/master
Inline type annotation function
commit3187e59063a102b9d661631ba0998b001c9e0788
authorEdwin Brady <edwin.brady@gmail.com>
dateWed 28 Nov 2012, 15:02 (14 years ago)
parentf9e06055501396
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