From a2522fd3166405f30372f81fe86f92878dc4db63 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 10 Apr 2021 15:13:05 -0700 Subject: [PATCH] test: for issue #387 closes #387 --- tests/lean/run/387.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 tests/lean/run/387.lean diff --git a/tests/lean/run/387.lean b/tests/lean/run/387.lean new file mode 100644 index 0000000000..4125badd8c --- /dev/null +++ b/tests/lean/run/387.lean @@ -0,0 +1,16 @@ +-- + +axiom p {α β} : α → β → Prop +axiom foo {α β} (a : α) (b : β) : p a b + +example : p 0 0 := by simp [foo] +example (a : Nat) : p a a := by simp [foo a] +example : p 0 0 := by simp [foo 0] +example : p 0 0 := by simp [foo 0 0] +example : p 0 0 := by + simp [foo 1] -- will not simplify + simp [foo 0] +example : p 0 0 ∧ p 1 1 := by + simp [foo 1] + traceState + simp [foo 0]