macro for applying list of arguments

Stream: Is there code for X?

[Asei Inoue]

set_option linter.unusedVariables false

def foo (a1 a2 a3 a4 a5 a6 a7 : String) : IO Unit :=
  IO.println "many arguments!"

def args := ["one", "two", "three", "four", "five", "six", "seven"]

-- some macro definition...
-- Here it is temporarily defined as infix.
infix:70 " apply " => sorry

#check (foo apply args)

[Yaël Dillies]

Are you looking for docs#Lean.mkAppN ?

[Asei Inoue]

@Yaël Dillies Thank you! but argument type of mkAppN is Expr...

[Yaël Dillies]

You can turn your args into an Array Expr if you want to

[Patrick Massot]

This would be a very inefficient way

[Patrick Massot]

Asei is right that they need something purely syntactic.

[Yaël Dillies]

Maybe it would be good to un #xy

[Patrick Massot]

It is easy to do if you know that kind of things. I’ll wait a bit to see if someone who can write the solution without firing up Lean shows up. Other I’ll take a look.

[Eric Wieser]

No metaprogramming needed:

import Mathlib
set_option linter.unusedVariables false

def foo (a1 a2 a3 a4 a5 a6 a7 : String) : IO Unit :=
  IO.println "many arguments!"

def args := ["one", "two", "three", "four", "five", "six", "seven"]

def apply (l : List α) (f : Function.OfArity α β l.length) : β :=
  match l with
  | [] => f
  | x :: xs => apply xs (f x)

#eval (apply args foo : IO Unit)

[Asei Inoue]

@Eric Wieser Thank you! I also want to generalise to cases where the argument types are not necessarily the same.

[Eric Wieser]

Then you can't use a list

[Asei Inoue]

@Eric Wieser indeed, you're right...!!

[Eric Wieser]

You might find some of the declarations near docs#Function.OfArity interesting

[Eric Wieser]

docs#Function.FromTypes.uncurry especially