Fixed failing regression test due to new syntax extension rules
commitdcbab5e67bc2256317b5686ab805dd5cac7c0cce
authorAhmad Salim Al-Sibahi <asal@itu.dk>
dateTue 24 Feb 2015, 21:42 (12 years ago)
parent13073a1
test/reg041/ott.idr+1−1
@@ -37,6 +37,6 @@ EQ two False two False = one
3737EQ (pi s t) f (pi s' t') g = pi s $ \x => pi s' $ \y => EQ s x s' y ~> EQ (t x) (f x) (t' y) (g y)
3838EQ _ _ _ _ = zero
3939
40−example : <| id == id in (two ~> two) |>
40+example : <| (id == id in (two ~> two)) |>
4141example = ?prf
4242