How do I fill in autoParam in Expr?

Stream: new members

[Kenny Lau]

import Mathlib

open Lean Meta

theorem foo (n m : ℕ) (h : n ≤ m := by decide) : n ≤ m := h

elab "test%" : term =>
  mkAppM ``foo #[mkNatLit 2, mkNatLit 3]

#check test% -- @foo 2 3 : autoParam (2 ≤ 3) _auto✝ → 2 ≤ 3

I would like to generate the expression foo 2 3 with h filled in, how do I do that?

[Aaron Liu]

Try mkAppOptM

[Kenny Lau]

it seems to just make a metavariable

[Kenny Lau]

i don't think the Opt in the name stands for optParam

[Aaron Liu]

Found the elab code that usually handles this https://github.com/leanprover/lean4/blob/ed4d453346c223546289d4b2d3bd8d2b4d1cf551/src/Lean/Elab/App.lean#L661-L686

[Alfredo Moreira-Rosa]

elab "test%" : term => do
  return ← Lean.Elab.Term.elabTerm (← `(foo 2 3)) none

[Aaron Liu]

that doesn't work for something more complicated than 2 and 3

[Alfredo Moreira-Rosa]

yes, but the idea is to use elabTerm, building complex terms is easy with other intermediate steps.

[Aaron Liu]

the problem is that you have to reflect expr back into syntax for this to work