max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: fix to new name for "Associative" in ac_rfl / ac_nf docstring (#10458)

Browse source 
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`.
This commit is contained in:
Alex Meiburg 2025-09-23 01:52:05 -04:00 • committed by GitHub
parent eabd7309b7
commit 8f9966ba74
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Init/Tactics.lean
View file

@ -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