From 52b6a0408812252e27f6cdc16c14a83ebe21adb4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 3 Jan 2022 07:57:16 -0800 Subject: [PATCH] test: for #916 --- tests/lean/916.lean | 4 ++++ tests/lean/916.lean.expected.out | 1 + 2 files changed, 5 insertions(+) create mode 100644 tests/lean/916.lean create mode 100644 tests/lean/916.lean.expected.out diff --git a/tests/lean/916.lean b/tests/lean/916.lean new file mode 100644 index 0000000000..7223b859ab --- /dev/null +++ b/tests/lean/916.lean @@ -0,0 +1,4 @@ +example : Id Nat := do + let mut x := 1 + have x : Nat := 2 + x diff --git a/tests/lean/916.lean.expected.out b/tests/lean/916.lean.expected.out new file mode 100644 index 0000000000..1de8b68bfb --- /dev/null +++ b/tests/lean/916.lean.expected.out @@ -0,0 +1 @@ +916.lean:3:2-3:19: error: mutable variable 'x' cannot be shadowed