Metavariables in unambiguous expressions

Stream: lean4

[Leni Aniva]

When this expression is parsed, why does it generate metavariables?

(2: Nat) <= (5: Nat)

this generates @LE.le ? ? (@OfNat.ofNat ? 2 ?) (@OfNat.ofNat ? 5 ?)

[Eric Wieser]

Can you give a mwe?

[Marcus Rossel]

This at least prints the expected result:

import Lean
open Lean Meta Elab Term

set_option pp.explicit true in
#eval show TermElabM Unit from do
  let e ← elabTerm (← `((2: Nat) <= (5: Nat))) none
  println! ← ppExpr e -- @LE.le Nat instLENat 2 5