How to get expected type in short elab syntax?

Stream: new members

[Jakub Nowak]

In this example copied from "Metaprogramming in Lean 4". Is it possible to get type? that is available in myTerm1Impl using the short elab syntax below?

syntax (name := myterm1) "myterm_1" : term

def mytermValues := [1, 2]

@[term_elab myterm1]
def myTerm1Impl : TermElab := fun stx type? => do
  mkAppM ``List.get! #[.const ``mytermValues [], mkNatLit 0] -- `MetaM` code

#eval myterm_1 -- 1

-- Also works with `elab`
elab "myterm_2" : term => do
  mkAppM ``List.get! #[.const ``mytermValues [], mkNatLit 1] -- `MetaM` code

#eval myterm_2 -- 2

[Jakub Nowak]

That works ig let type? := ‹Option Expr›.

[Sebastian Miele]

elab "myterm_2" : term <= type => do
  logInfo type
  pure <| mkNatLit 1

#eval (myterm_2) -- `type` is a metavariable
#eval (myterm_2 : Nat) -- `type` is ``Nat`

The reference manual seems to not have documentation on elab, yet. But its elaborator can be found asLean.Elab.Command.elabElab. Metaprogramming in Lean 4 mentions the <= type syntax at the very bottom of the Elaboration chapter, just before the exercises.

[Jakub Nowak]

Hm, but type is Lean.Expr in this case. Reading Lean.Elab.Command.elabElab it looks like it's using Lean.Elab.Term.withExpectedType, which will error when expected type is not known. So it's not the same.

I could probably use both elab "myterm_2" : term => commonLogic .none and elab "myterm_2" : term <= type => do commonLogic (.some type).

I think I'll just use let type? := ‹Option Expr›. It looks a bit hacky, but I think it's ok.

[Robin Arnez]

Yeah, idk how you're supposed to do it but I always just used ‹_› for this purpose (e.g. as in elabTerm stx ‹_›)