Syntax for a list of terms

Stream: lean4

[Scott Morrison]

I would like to write a tactic which takes a list of expressions, and I think it makes sense for the caller to actually write the list notation.

That is, I would like the caller to write something like

my_fancy_tac using [37, "foo", [1,2]]

I would then like to obtain the List Expr obtained elaborating each of these.

I could do just by asking for a single term at the Syntax level, elaborating that, then decomposing the resulting Expr object to see if it represents a List. But would it be better to express this all at Syntax level? If so, how would I do so?

[Scott Morrison]

I'm not sure here whether I ought to avoid mucking about with Exprs, or avoid rewriting a List parser.

[Scott Morrison]

e.g. the "single term" method perhaps looks like:

syntax "my_fancy_tac" "using" term : tactic

partial def Expr_to_List_Expr : Expr → List Expr
| e => match e.getAppFnArgs with
  | (`List.cons, #[_, h, t]) => h :: (Expr_to_List_Expr t)
  | _ => []

elab_rules : tactic
  | `(tactic| my_fancy_tac using $t:term) => do
    let e ← Lean.Elab.Term.elabTerm t none
    let l := Expr_to_List_Expr e
    for f in l do
      logInfo f

example : True := by
  my_fancy_tac using [37,57] -- Prints 37 then 57.
  trivial

[Leonardo de Moura]

What about this?

import Lean

open Lean

syntax "my_fancy_tac" "using" "[" term,* "]" : tactic

elab_rules : tactic
  | `(tactic| my_fancy_tac using [ $ts:term,* ]) => do
    let es ← ts.getElems.mapM (Lean.Elab.Term.elabTerm · none)
    for f in es do
      logInfo f

example : True := by
  my_fancy_tac using [37, "foo",  [1,2]]
  trivial