tactic state in custom command

Stream: lean4

[Alexander Bentkamp]

Hello, I am trying to create a custom command. I would like the user to provide a proof, either in term or in tactic mode. But unfortunately when using tactic mode, the tactic state is invisible:

import Lean

open Lean
open Lean.Elab
open Lean.Elab.Command

syntax (name:=testCommand)
  "#test" term : command

@[commandElab testCommand] def elabTestCommand : CommandElab
| `(#test $expr) => do
  liftTermElabM none do
    let e ← Term.elabTerm expr (some (mkConst ``Nat))
    ()
| _ => throwUnsupportedSyntax

#test by
  show Nat
  exact 0

-- Why does it not show "⊢ Nat"?

What am I missing?

[Wojciech Nawrocki]

It seems like this happens because that, by itself, the by elaborator does nothing more than registering an mvar. Note the term isn't elaborated any further than that, for example

#test by
  show Nat
  exact "abc"

gives no error whereas

#test ("abc" : Nat)

does. You may want to use elabTermAndSynthesize to ensure tactic code is executed.

[Alexander Bentkamp]

Ah, that's great! Thanks!

[Alexander Bentkamp]

Unfortunately, elabTermAndSynthesize doesn't enforce the expected type in term mode. There is also a functionelabTermEnsuringType, but that one does not support tactic mode. I have written my own combination of the two now (below). Is such a function already defined somewhere?

def elabTermAndSynthesizeEnsuringType (stx : Syntax) (expectedType? : Option Expr) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
  let e ← elabTermAndSynthesize stx expectedType?
  withRef stx <| ensureHasType expectedType? e errorMsgHeader?