From 63decd445c5b07980a088951fd52f2f12ccaa53e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 10 Dec 2021 13:13:03 -0800 Subject: [PATCH] chore: fix test --- tests/lean/770.lean.expected.out | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tests/lean/770.lean.expected.out b/tests/lean/770.lean.expected.out index 7032639714..540ab2ff51 100644 --- a/tests/lean/770.lean.expected.out +++ b/tests/lean/770.lean.expected.out @@ -1 +1,2 @@ -file '770.lean' not found +770.lean:1:25-3:40: error: invalid 'do' notation, expected type is not a monad application + Nat