Elaborate ‹...›

Stream: lean4

[Marcus Rossel]

How does one correctly elaborate a term of the form ‹...›. The following example doesn't work:

import Lean
open Lean Meta Elab Term

elab "test" t:term : tactic => do
  let ex ← elabTerm t none
  let ty ← inferType ex
  IO.println (← ppExpr ex)
  IO.println (← ppExpr ty)

example (h : ∀ x : Nat, x = x) : True := by
  test ‹∀ _, _›
  -- ?m.1242
  -- (x : ?m.1237) → ?m.1241 x

Also, adding instantiateMVars didn't help.

[Yaël Dillies]

Does ‹∀ _ : ℕ, _› work?

[Marcus Rossel]

Nope

[Yaël Dillies]

and ‹∀ _ : ℕ, _ = _›?

[Yaël Dillies]

I think you're just hitting the limitations of higher order unification.

[Marcus Rossel]

Also nope. Even going full ‹∀ x : Nat, x = x› doesn't work.
But writing something like have g := ‹_› figures out that g is h, so I don't think unification is the problem here.

[Alex J. Best]

You code is using Term.elabTerm, if you use Tactic.elabTerm instead it works

[Marcus Rossel]

Thanks! What can Tactic.elabTerm do that Term.elabTerm can't? I.e. when should one use one over the other?

[Mario Carneiro]

Tactic.elabTerm wraps Term.elabTerm in withSynthesize, which synthesizes delayed metavariables. ‹T› is syntax for (by assumption : T) and by always creates a delayed metavariable, so you have to call withSynthesize or synthesizeSyntheticMVarsNoPostponing to actually get it to resolve