From 8f9966ba74fe3145a4e80e1a620a9c7741e830c0 Mon Sep 17 00:00:00 2001 From: Alex Meiburg Date: Tue, 23 Sep 2025 01:52:05 -0400 Subject: [PATCH] doc: fix to new name for "Associative" in ac_rfl / ac_nf docstring (#10458) This PR fixes the docstring for ac_rfl and ac_nf to correctly refer to `Std.Associative` instead of the old name `Associative`; ditto `Commutative`. --- src/Init/Tactics.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 05a3843fde..5588fcf532 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -436,8 +436,8 @@ macro "rfl'" : tactic => `(tactic| set_option smartUnfolding false in with_unfol /-- `ac_rfl` proves equalities up to application of an associative and commutative operator. ``` -instance : Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩ -instance : Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩ +instance : Std.Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩ +instance : Std.Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩ example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by ac_rfl ``` @@ -1563,8 +1563,8 @@ syntax (name := normCastAddElim) "norm_cast_add_elim" ident : command list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-` can also be used, to signify the target of the goal. ``` -instance : Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩ -instance : Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩ +instance : Std.Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩ +instance : Std.Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩ example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by ac_nf