引数を展開して関数に流し込むのは可能か?

[Seasawher]

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"]

-- 明らかに重複がある
#eval foo args[0] args[1] args[2] args[3] args[4] args[5] args[6]

[Seasawher]

マクロを書けばできそう

[Seasawher]

see: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/macro.20for.20applying.20list.20of.20arguments/near/444939240

[Seasawher]

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)