@@ -1,9 +1,8 @@
1−myid : a -> a
1+myid : (a : Type) -> a -> a
2−myid x = x
2+myid _ x = x
4−-- FIXME: Raw TT quotations currently unsupported in parser
5−--idid : (a : Type) -> a -> a
4+idid : (a : Type) -> a -> a
6−--idid = myid ![myid]
5+idid = myid _ myid
8app : (a -> b) -> a -> b
7app : (a -> b) -> a -> b
9app f x = f x
8app f x = f x
@@ -12,7 +11,7 @@ foo : a -> b -> c -> d -> e -> e
12foo a b c d e = e
11foo a b c d e = e
14doapp : a -> a
13doapp : a -> a
15−doapp x = app myid x
14+doapp x = app (myid _) x