Elaborate term with info view

Stream: lean4

[Patrick Massot]

One last meta question for today. I have no problem creating commands that consume terms but I can't use tactic mode. How do commands like def or theorem tell Lean the type they expect? If I type:

import Lean

open Lean Elab Command

elab "Test" typ:term ":=" val:term : command => do
  -- actually do something here?
  pure ()

Test Nat := by
  -- I'd like the info view to show "⊢ Nat" here.
  sorry

I know I can define aliases for def and theorem but this isn't what I want to do here.

[Sebastian Ullrich]

It's the expected type when elaborating val (which you currently don't do), i.e. from elabTerm

[Patrick Massot]

I tried things like calling term elaboration inside the command. For instance

elab "Test" typ:term ":=" val:term : command => do
  let e ← liftTermElabM do
    let typ ← elabTerm typ none
    return (← elabTermEnsuringType val typ)
  pure ()

Test Nat := by
  exact "Yo"

But there is no error at all in this example

[Patrick Massot]

and no info view display either.

[Henrik Böving]

I was expecting something similar to work as well:

elab "Test" typ:term ":=" val:term : command => do
  let ty ← liftTermElabM <| Term.elabType typ
  let res ← liftTermElabM <| Term.elabTermEnsuringType val ty
  IO.println s!"{ty}, {res}"

it surprises me quite a lot that this doesn't error as patrick expects, why is that?

[Sebastian Ullrich]

You also need to wrap it in withSynthesize to actually force the tactic block to run

[Patrick Massot]

This seems to work much better!

[Patrick Massot]

Thanks Sebastian!

[Sebastian Ullrich]

Not sure if liftTermElabM should imply withSynthesize. It's also worth mentioning that you need runTermElabM instead for proper support of variables.

[Patrick Massot]

Thanks. I know this variable handling difference between liftTermElabM and runTermElabM, Leo explained it a couple of weeks ago and he took the opportunity to write docstrings for those two functions.

[Patrick Massot]

Maybe those docstrings should mention withSynthesize.

[Sebastian Ullrich]

Those docstrings are definitely helpful. Without them I wouldn't have known the difference either, haha.