Parsing lists with optional tokens

Stream: lean4

[Damiano Testa]

Dear All,

I am porting move_add to Lean 4. For this, I would like to pass to the tactic a list of terms, optionally preceded by a left arrow. What is the syntax to achieve this?

Example:

example : True := by
  move_add [a, ← b, c]
--> I would like convert the above into `(a, false), (b, true), (c, false)`.

I know how to elabTerm the a, b, c, if I do not put the optional left arrow, but I cannot do the whole parsing...

Thanks!

[Damiano Testa]

I think that this is the syntax:

syntax "move_add" (colGt "←"? term),* : tactic

but I do not know how to "catch" it in the elab_rules command...

[Alex J. Best]

Well you can resuse the internals of rewrite a bit, seeing as its quite similar

open Lean Parser Tactic Elab Term PrettyPrinter
elab "move_add" rws:rwRuleSeq : tactic =>
  match rws with
  | `(rwRuleSeq| [$rs,*]) =>
    for r in rs.getElems do
      let r : Syntax := r
      logInfo <| toString (← delab (← elabTerm r[1] none), r[0]!.isNone)
  | _ => failure

example (a b c : ℕ) : a + b = b := by
  move_add [a, ← b, c]

[Damiano Testa]

Alex, thank you very much! I'll try it as soon as I am back at my computer.

[Damiano Testa]

Alex, it works great! Here is what I ended up using:

open Lean Parser Tactic Elab Term PrettyPrinter
elab "move_add" rws:rwRuleSeq : tactic =>
  match rws with
  | `(rwRuleSeq| [$rs,*]) => do
    let pairs := ← rs.getElems.mapM fun r => do
      let r : Syntax := r
      let a := ← Term.elabTerm r[1]! none
      return (a, r[0]!.isNone)
    logInfo m!"{pairs}"
  | _ => failure

example (a b c : ℤ) : a + b = b := by
  move_add [a, ← b, c]