From a9628f2a80ebb768d7ca5a0253eee57362311d7c Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Wed, 21 Feb 2024 12:38:43 -0800 Subject: [PATCH] suggestion --- src/Lean/Parser/Tactic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean index e2cc01dcea6f..7b32c4579036 100644 --- a/src/Lean/Parser/Tactic.lean +++ b/src/Lean/Parser/Tactic.lean @@ -78,8 +78,8 @@ Limitations: - Because this uses kernel reduction to evaluate the term, `Decidable` instances defined by well-founded recursion might not work, because evaluating them requires reducing proofs. The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions. - These can appear for instances defined using the `rw` and `simp` tactics for example -- - make sure to use definitions such as `decidable_of_iff` instead. + These can appear for instances defined using tactics (such as `rw` and `simp`). + To avoid this, use definitions such as `decidable_of_iff` instead. ## Examples