Get `Expr` from arbitrary definition?

Stream: lean4

[Vasilii Nesterov]

Hello! Is it possible in Lean to obtain the Expr object from an arbitrary let definition? I see that there is a ToExpr class for this purpose, but it works only with a small set of types.

[Jovan Gerbscheid]

Are you looking for something like the Qq library? I allows you to make an Expr object like this:

import Qq
open Qq
/-
Lean.Expr.app
  (Lean.Expr.app
    (Lean.Expr.app
      (Lean.Expr.app
        (Lean.Expr.app
          (Lean.Expr.app
            (Lean.Expr.const `HAdd.hAdd [Lean.Level.zero, Lean.Level.zero, Lean.Level.zero])
            (Lean.Expr.const `Nat []))
          (Lean.Expr.const `Nat []))
        (Lean.Expr.const `Nat []))
      (Lean.Expr.app
        (Lean.Expr.app (Lean.Expr.const `instHAdd [Lean.Level.zero]) (Lean.Expr.const `Nat []))
        (Lean.Expr.const `instAddNat [])))
    (Lean.Expr.app
      (Lean.Expr.app
        (Lean.Expr.app (Lean.Expr.const `OfNat.ofNat [Lean.Level.zero]) (Lean.Expr.const `Nat []))
        (Lean.Expr.lit (Lean.Literal.natVal 1)))
      (Lean.Expr.app (Lean.Expr.const `instOfNatNat []) (Lean.Expr.lit (Lean.Literal.natVal 1)))))
  (Lean.Expr.app
    (Lean.Expr.app
      (Lean.Expr.app (Lean.Expr.const `OfNat.ofNat [Lean.Level.zero]) (Lean.Expr.const `Nat []))
      (Lean.Expr.lit (Lean.Literal.natVal 1)))
    (Lean.Expr.app (Lean.Expr.const `instOfNatNat []) (Lean.Expr.lit (Lean.Literal.natVal 1))))

-/
#eval q(1+1)

[Vasilii Nesterov]

Thanks, that's almost what I was looking for! Can I use it with local definitions? Something like this:

def foo : Expr :=
  let n : ℕ := 1 + 1
  q(n)

[Eric Wieser]

You can do

def foo : Expr :=
  let n : Q(ℕ) := q(1 + 1)
  q($n)