listing explicit argument types

Stream: metaprogramming / tactics

[Damiano Testa]

Dear All,

I have been struggling with the following problem. Whenever I want to apply a function in Lean, I am expected to give it its explicit arguments. In the background, Lean figures out the implicit/typeclass inputs automatically.

Is there a consistent way to get the list of expressions corresponding to the explicit arguments of a function?

E.g. on input has_add.add I would like to have twice the same type and skip the typeclass argument.

I have been failing to get this to work consistently and systematically. If the question is not clear, I can provide the code that I have, but it is long, messy and dubious.

Ah, as the stream suggests, I'm eventually looking for a way to do this in meta!

Thanks!

[Eric Wieser]

docs#tactic.fold_explicit_args

[Damiano Testa]

Thanks a lot! This looks like what I was looking for!

[Damiano Testa]

For the record, Eric's suggestion seems to be working exactly as I wanted! Here is an example (mostly for my benefit!):

example : 4 + 5 = 3 * 3 :=
by do `(%%lhs = %%rhs) ← target,
  trace $ fold_explicit_args lhs ([] : list expr) (λ ll e, return $ ll ++ [e]),
  trace $ fold_explicit_args rhs ([] : list expr) (λ ll e, return $ ll ++ [e])
/-
[4, 5]
[3, 3]
-/

[Eric Wieser]

It does seem odd that we don't just have get_explicit_args : list expr, from which you could recover the fold version via docs#list.mfoldl; I guess it's either an efficiency thing, or a bootstrapping thing.

[Damiano Testa]

The file that you linked to seems to aim directly for this result, so I am guessing that it is the bootstrapping thing: you have to start somewhere.

[Alex J. Best]

I think in general the meta-programming / parts of the library are less thought out and consistent than the maths stuff, people just added precisely what they needed, when they needed it for a lot of these defs.