How to `have` an `Expr`?

Stream: metaprogramming / tactics

[Alexander Bentkamp]

Hello, I would like to invoke have within metaprogramming like this:

import Lean

open Lean Meta Elab Tactic

elab "test" : tactic => do
    let expr : Expr := mkConst `Nat.zero_lt_one
    evalTactic $ ← `(tactic| have h := Nat.zero_lt_one) -- how to use `expr` here?

example : False := by
  test
  sorry

I don't have the expression I want to "have" as Syntax, but as an Expr. How can I make this work?

Ideally, I would also like to know the FVarId introduced by the have.

[Henrik Böving]

have is just a let binder that is non dependent. So you would call Lean.Meta.withLetDecl with nondep := true and then Lean.Meta.mkLetFVars to make the binder

[Alexander Bentkamp]

Hm, this works, but I didn't need to use Lean.Meta.mkLetFVars. Is this correct?

import Lean

open Lean Meta Elab Tactic

#check Lean.Meta.withLetDecl
#check Lean.Meta.mkLetFVars

elab "test" : tactic => do
    let mvar ← getMainGoal
    let mvarType ← inferType (mkMVar mvar)
    let expr : Expr := mkConst `Nat.zero_lt_one
    Lean.Meta.withLetDecl (nondep := true) `h (← inferType expr) expr fun fvar => do
      let newMVar ← mkFreshExprMVar mvarType
      mvar.assign newMVar
      replaceMainGoal [newMVar.mvarId!]

example : False := by
  test
  sorry

[Henrik Böving]

Ah, to do specifically that thing no, but if you want to do a have followed by some other stuff in a general expression you would have to. For the specific use case of just injecting new hypotheses into a goal there is also Lean.MVarId.assertHypotheses

[Alexander Bentkamp]

Ah, great, that's what I was looking for. Thanks!