From 75872189ccec00a01c14e7a3164d881cfe86502d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Aug 2021 13:10:58 -0700 Subject: [PATCH] chore: fix test --- tests/lean/PPRoundtrip.lean.expected.out | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/tests/lean/PPRoundtrip.lean.expected.out b/tests/lean/PPRoundtrip.lean.expected.out index 8984b43295..15dc1aae5e 100644 --- a/tests/lean/PPRoundtrip.lean.expected.out +++ b/tests/lean/PPRoundtrip.lean.expected.out @@ -54,12 +54,11 @@ decide (1 < 2) || true id (fun a => a) 0 typeAs Nat - (do - let x ← pure 1 + (let x := 1; + do discard (pure 2) let y : Nat := 3 - pure (x + y) : - Id Nat) + pure (x + y)) typeAs (Id Nat) (pure 1 >>= pure) (0 ≤ 1) = False