Many1 antiquotations

Stream: lean4

[Wojciech Nawrocki]

Is it possible to construct a tuple, or a list of arguments to a function, with the [..]* antiquotation? Here is what I'm trying that fails:

open Lean Elab Command in
elab "foo_cmd" : command =>
    Command.liftTermElabM none do
        let foos := #[mkIdent `Foo₁, mkIdent `Foo₂]
        let s : Syntax ← `([ $[$foos],* ])
        /- [Foo₁, Foo₂] -/
        let s : Syntax ← `(( $[$foos],* ))
        /- expected '(', ')', '*', '_' or identifier -/
        let s : Syntax ← `( myFunc $[$foos]* )
        /- expected ')' or '|' -/

[Mac]

Wojciech Nawrocki said:

        /- [Foo₁, Foo₂] -/
        let s : Syntax ← `(( $[$foos],* ))

The problem here is that it doesn't know how many elements to expect. The empty tuple () is a separate syntax so you need to provide a least one element as a given (e.g., (( foo, $[$foos],* ))) to get it to auto infer the kind.

[Wojciech Nawrocki]

I see, though for applications the myFunc args parse doesn't work out with args an antiquote. I am using Syntax.mkApp instead.

[Wojciech Nawrocki]

Ah, `(myFunc $foos*).

[Sebastian Ullrich]

Yeah, the function argument splice is a "fun" gotcha: the parser says that arguments have to be preceded by whitespace, and so this holds for splices as well.

`(myFunc $[ $foos]*)