diff --git a/tests/lean/modBug.lean.expected.out b/tests/lean/modBug.lean.expected.out index 94945a5293..389d68e4a0 100644 --- a/tests/lean/modBug.lean.expected.out +++ b/tests/lean/modBug.lean.expected.out @@ -1,6 +1,8 @@ -modBug.lean:1:8-1:20: error: application type mismatch +modBug.lean:1:32-1:61: error: application type mismatch Nat.zeroNeOne (Nat.modZero 1) -argument has type +argument + Nat.modZero 1 +has type 1 % 0 = 1 -but function has type - 0 = 1 → False +but is expected to have type + 0 = 1