From d32475d62689883c34660c0692468195d18f3a49 Mon Sep 17 00:00:00 2001 From: brett koonce Date: Fri, 29 May 2026 08:39:25 -0500 Subject: [PATCH] Update Tactics.lean/rm dupe sentence Fixes duplicate entry in docs downstream: https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tactic-Reference/#decide Reported in Zulip: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Discussion.20thread.20for.20Lean.20Language.20Reference/near/598496721 --- src/Init/Tactics.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 3cc320afa4ea..1a42292f405c 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -1410,7 +1410,7 @@ Options: It has two key properties: (1) since it uses the kernel, it ignores transparency and can unfold everything, and (2) it reduces the `Decidable` instance only once instead of twice. - `decide +native` uses the native code compiler (`#eval`) to evaluate the `Decidable` instance, - admitting the result via an axiom. This can be significantly more efficient than using reduction, but it is at the cost of increasing the size + admitting the result via an axiom. This can be significantly more efficient than using reduction, but it is at the cost of increasing the size of the trusted code base. Namely, it depends on the correctness of the Lean compiler and all definitions with an `@[implemented_by]` attribute.