Postpone elaboration as long as possible

Stream: lean4

[Eric Wieser]

Is it possible for an elaborator to delay until all other metavariables have been filled? The closest I could come up with was

import Lean

open Lean

syntax (name := elab_last) "elab_last(" term ")" : term

@[term_elab elab_last]
def elab_lastElab : Elab.Term.TermElab := fun stx ty? =>
match stx with
  | `(elab_last($stx:term)) => do
      Lean.Elab.Term.postponeElabTerm (← `(by exact $stx)) ty?
  | _ => Elab.throwUnsupportedSyntax

[Eric Wieser]

This works reasonably well, but fails when something else is competing by also using by exact to postpone elaboration:

-- succeeds, LHS is treated as an Int
example : 1 = (1 : Int) := sorry

-- intended behavior
/--
error: type mismatch
  1
has type
  Int : Type
but is expected to have type
  Nat : Type
-/
#guard_msgs in
example : 1 = elab_last((1 : Int)) := sorry

-- intended behavior
/--
error: type mismatch
  1
has type
  Int : Type
but is expected to have type
  Nat : Type
-/
#guard_msgs in
example : elab_last((1 : Int)) = 1 := sorry

-- succeeds, but should not: the `by exact` runs after `elab_last`
example : elab_last((1 : Int)) = (by exact 1) := sorry

[Thomas Murrills]

Silly "solution": by exact (by exact $stx) :sweat_smile: (This doesn't work, but honestly I'd kind of expect it to in this case...)

[Eric Wieser]

I also tried that and was surprised it didn't work!

[Markus Himmel]

Probably not very robust, but the naive

  | `(elab_last($stx:term)) => do
      Elab.Term.tryPostpone
      Lean.Elab.Term.postponeElabTerm (← `(by exact $stx)) ty?

seems to work in your example at least.