normal code => explicit Expr?

Stream: lean4

[Evgenia Karunus]

Is there a method that returns the underlying Expr in either Lean 3 or Lean 4?
For example, getExpr (1+2) would return mkApp (mkApp (Expr.const 'Nat.add []) (mkNatLit 1)) (mkNatLit 2).

[Horațiu Cheval]

You can do that with elabTerm and its variants

[Horațiu Cheval]

import Lean

open Lean

#eval show MetaM _ from do
  let stx : Syntax ← `((1 + 2 : Nat))
  let e := Elab.Term.elabTermAndSynthesize stx none
  return e

[Horațiu Cheval]

But the underlying Expr of 1 + 2 seems to be a lot more intimidating than your example :)

[Horațiu Cheval]

Actually I think TermElabM is the right monad for that

def getExpr (stx : Syntax) : Elab.TermElabM Expr := do
  let e := Elab.Term.elabTermAndSynthesize stx none
  e

#eval show Elab.TermElabM Expr from do getExpr (← `((1 + 2 : Nat)))

[Notification Bot]

Evgenia Karunus has marked this topic as unresolved.