Reinstate universe checking in test002
commitf6d3e1c51a96956c3e57c64d09b10b3941902943
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateTue 19 Nov 2013, 14:52 (13 years ago)
parent76a3fda
test/test002/expected+2
@@ -0,0 +1,2 @@
1+test002.idr:5:6:Universe inconsistency
2+test002.idr:5:6:Universe inconsistency
test/test002/test002.idr+5−6
@@ -1,9 +1,8 @@
1−myid : a -> a
2−myid x = x
1+myid : (a : Type) -> a -> a
2+myid _ x = x
33
4−-- FIXME: Raw TT quotations currently unsupported in parser
5−--idid : (a : Type) -> a -> a
6−--idid = myid ![myid]
4+idid : (a : Type) -> a -> a
5+idid = myid _ myid
76
87app : (a -> b) -> a -> b
98app f x = f x
@@ -12,7 +11,7 @@ foo : a -> b -> c -> d -> e -> e
1211foo a b c d e = e
1312
1413doapp : a -> a
15−doapp x = app myid x
14+doapp x = app (myid _) x
1615
1716{-
1817