diff --git a/tests/lean/t3.lean.expected.out b/tests/lean/t3.lean.expected.out index 5f450be553..7c65a357fd 100644 --- a/tests/lean/t3.lean.expected.out +++ b/tests/lean/t3.lean.expected.out @@ -10,7 +10,7 @@ Type Type Type t3.lean:26:10: error: invalid namespace declaration, atomic identifier expected -t3.lean:27:1: error: invalid declaration name 'full.name.U', identifier must be atomic +t3.lean:27:0: error: invalid declaration name 'full.name.U', identifier must be atomic Type Type t3.lean:35:2: error: universe level alias 'u' shadows existing global universe level diff --git a/tests/lean/t9.lean.expected.out b/tests/lean/t9.lean.expected.out index 15f8587be1..e02d98ed3e 100644 --- a/tests/lean/t9.lean.expected.out +++ b/tests/lean/t9.lean.expected.out @@ -1,3 +1,3 @@ add a (mul b a) : N -t9.lean:16:8: error: invalid expression +t9.lean:16:7: error: invalid expression add a (mul b a) : N