Constructing syntax for natural number literal

Stream: metaprogramming / tactics

[Segev Elazar Mittelman]

Hi I attempted to create a TSyntax for a natural number literal given a Literal of the form .natVal n I did

def mkLiteral (l : Literal) : MetaM (TSyntax `term) :=
  match l with
  | .natVal n => `($(Syntax.mkNumLit (toString n)))
  | .strVal s => `($(Syntax.mkStrLit s))

But when I to elaborate something which uses mkLiteral, it creates for instance, "Eq n_1 (OfNat.ofNat («5»))", and I get this error:

Unknown identifier «5»

Am I constructing the syntax wrong?

[Bhavik Mehta]

I think you want to use Syntax.mkNatLit in the first case

[Segev Elazar Mittelman]

Unfortunately both choices display the error.

[Robin Arnez]

I can't tell what's wrong, it seems to work on my side, what do you do with the output?

[Segev Elazar Mittelman]

Try

#eval (Eq 1 (OfNat.ofNat («5»)))

[Aaron Liu]

what is the expected output and what is the actual output

[Robin Arnez]

I mean this works?

import Lean

open Lean Meta

def mkLiteral (l : Literal) : MetaM (TSyntax `term) :=
  match l with
  | .natVal n => `($(Syntax.mkNumLit (toString n)))
  | .strVal s => `($(Syntax.mkStrLit s))

run_elab
  let num ← mkLiteral (.natVal 5)
  let term ← `(Eq 1 (OfNat.ofNat $num))
  Lean.logInfo (← Lean.Elab.Term.elabTerm term none)

[Segev Elazar Mittelman]

Hm, I suspect this issue is caused elsewhere. I'll continue looking.