Lean4
/-- Adds hypotheses to the context, turning them into goals to be proved later if their proof terms
aren't provided (`t: Option Term := none`).
If the bound term is intended to be kept in the context, pass `keepTerm : Bool := true`. This is
useful when extending the `let` tactic, which is expected to show the proof term in the infoview.
-/
def haveLetCore (goal : MVarId) (name : TSyntax ``optBinderIdent) (bis : Array (TSyntax ``letIdBinder))
(t : Option Term) (keepTerm : Bool) : TermElabM (MVarId × MVarId) :=
let declFn := if keepTerm then MVarId.define else MVarId.assert
goal.withContext do
let n := optBinderIdent.name name
let elabBinders k := if bis.isEmpty then k #[] else elabBinders bis k
let (goal1, t, p) ←
elabBinders fun es ↦ do
let t ←
match t with
| none =>
mkFreshTypeMVar
| some stx =>
withRef stx do
let e ← Term.elabType stx
Term.synthesizeSyntheticMVars (postpone := .no)
instantiateMVars e
let p ← mkFreshExprMVar t MetavarKind.syntheticOpaque n
pure (p.mvarId!, ← mkForallFVars es t, ← mkLambdaFVars es p)
let (fvar, goal2) ← (← declFn goal n t p).intro1P
goal2.withContext do
Term.addTermInfo' (isBinder := true) name.raw[0] (mkFVar fvar)
pure (goal1, goal2)
