git.iko.soy/Idris-dev
on master help sign in
Fixed failing regression test due to new syntax extension rules
dcbab5eAhmad Salim Al-Sibahi
test/reg041/ott.idr+1−1
compare with master
unifiedsplit
@@ -37,6 +37,6 @@ EQ two False two False = one
37EQ (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)
37EQ (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)
38EQ _ _ _ _ = zero
38EQ _ _ _ _ = zero
39
39
40−example : <| id == id in (two ~> two) |>
40+example : <| (id == id in (two ~> two)) |>
41example = ?prf
41example = ?prf
42
42