From d8ca6d847b1cbdfdb1970cd3bf4eac7649dd2b3b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 20 Feb 2021 13:01:36 -0800 Subject: [PATCH] test: lost synthetic mvar issue --- tests/lean/run/pendingInstBug.lean | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 tests/lean/run/pendingInstBug.lean diff --git a/tests/lean/run/pendingInstBug.lean b/tests/lean/run/pendingInstBug.lean new file mode 100644 index 0000000000..a99999fa94 --- /dev/null +++ b/tests/lean/run/pendingInstBug.lean @@ -0,0 +1,8 @@ +class AddIdepotent (α : Type u) [Add α] : Prop where + add_id (x : α) : x + x = x + +export AddIdepotent (add_id) + +theorem tst [Add α] [AddIdepotent α] (x : α) : id (x + x + x) = x := by + rw [add_id, add_id] + simp [id]