code in docstring of `ac_rfl`

Stream: general

[Asei Inoue]

import Mathlib.Tactic

/-
syntax "ac_rfl"... [Lean.Parser.Tactic.acRfl]
  `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⟩

  example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by ac_rfl
  ```
-/
#help tactic ac_rfl

/-
invalid constructor ⟨...⟩, expected type must be an inductive type
  ∀ (a b c : ℕ),
    (fun x x_1 => x + x_1) ((fun x x_1 => x + x_1) a b) c = (fun x x_1 => x + x_1) a ((fun x x_1 => x + x_1) b c)
-/
instance : Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
instance : Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩

example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by ac_rfl

[Asei Inoue]

The code doesn't work, even though it is written exactly as described in the ac_rfl docstring.

[Markus Himmel]

The docstring should say Std.Associative and Std.Commutative. The two instances are in mathlib anyway (and they will be in the next version of core Lean), so you can just remove them in your code and the last line will work. I will update the docstring.

[Asei Inoue]

Thanks!