From 0f0f1407afc5509180bed89009bee895ce580944 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 17 Jun 2020 18:07:44 +0200 Subject: [PATCH] chore: fix test --- tests/lean/precissues.lean.expected.out | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/precissues.lean.expected.out b/tests/lean/precissues.lean.expected.out index 9a1e09264a..7af92953dd 100644 --- a/tests/lean/precissues.lean.expected.out +++ b/tests/lean/precissues.lean.expected.out @@ -8,7 +8,7 @@ precissues.lean:15:10: error: expected command 1 : Nat id ((λ (this : True), this) True.intro) : True 0=(λ (this : Nat), this) 1 : Prop -0=let x : Nat := 0 in x : Prop +0=let x : Nat := 0; x : Prop p↔¬q : Prop True=¬False : Prop p∧¬q : Prop