Define shorthand for `simp_all (config := ...)`

Stream: lean4

[Son Ho]

I'm often using simp_all with a custom configuration which is always the same, so I would like to introduce a shorthand for it. Basically, I want to introduce a notation my_simp_all ... which desugards to simp_all (config := {maxDischargeDepth := 1}) ... (for instance).
I tried the following but it doesn't work for a reason I don't quite understand (also I'm not sure this is the best way of doing this):

import Lean

open Lean

-- Same syntax as simpAll, but I removed the config
open Lean.Parser.Tactic
syntax (name := mySimpAll) "my_simp_all" (discharger)? (&" only")?
  (" [" withoutPosition((simpErase <|> simpLemma),*,?) "]")? : tactic

@[macro mySimpAll] def evalMySimpAll : Macro :=
  fun ctx =>
  match ctx.raw.getArgs.toList with
  | [discharger, only, lemmas] =>
    -- Introduce the config I want
    `(tactic| simp_all (config := {maxDischargeDepth := 1}) $discharger $only $lemmas)
   --                                                                   ^^^^^
   -- ERROR: "unexpected token '$'; expected ')'"
   -- Does the error come from the presence of `&` in `(&" only")?` above? How should I handle it?
  | _ => throwError "Unexpected"

[Jannis Limperg]

Here's a solution that's a bit dumb, but seems to work. Maybe there's a less dumb solution as well.

import Lean

open Lean Lean.Parser.Tactic Lean.Macro Lean.Syntax

syntax simpLemmas := "[" withoutPosition((simpErase <|> simpLemma),*,?) "]"

macro "my_simp_all" discharger:(discharger)? only:(&" only")?
    lemmas:(simpLemmas)? : tactic => do
  let cfg ← `(config| (config := { maxDischargeDepth := 1 }))
  match lemmas with
  | some lemmas =>
    match lemmas with
    | `(simpLemmas| [ $lemmas,* ]) =>
      if only.isSome then
        `(tactic| simp_all $cfg $[$discharger]? only [ $lemmas,* ])
      else
        `(tactic| simp_all $cfg $[$discharger]? [ $lemmas,* ])
    | _ => throwUnsupported
  | none =>
    if only.isSome then
      `(tactic| simp_all $cfg $[$discharger]? only)
    else
      `(tactic| simp_all $cfg $[$discharger]?)

example : 1 = 1 := by
  my_simp_all only [Nat.succ_eq_add_one]

[Son Ho]

Thanks Jannis! I think that will do :)

[Mauricio Collares]

There's also declare_simp_like_tactic

[Son Ho]

Mauricio Collares said:

There's also declare_simp_like_tactic

Nice, thanks!