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]*)

[James Gallicchio]

Necroposting on this thread to ask -- is there a core function to construct tuple syntax easier than what was described here?

I've got code that looks like

let hd := decrease[0]'_h
let tl := decrease[1:]
let lexOrd : Term ←
  if tl.size > 0 then
    `( ( $hd, $tl,* ) )
  else
    pure hd

and I suspect this is implementing something that exists elsewhere but I can't find :big_smile: