make a goal during elaboration

Stream: new members

[louq]

How do I make a goal in elab?

elab "myTactic" : tactic => do

let goalType ← mkAppM Nat.add [mkConst Nat, mkConst ``Nat]

Give me an example on lean4 web

[Chris Bailey]

Read this

import Lean
open Lean Meta

elab "myTactic" : tactic => do
  let goalType ← mkAppM ``True #[]
  let x ← liftMetaM (mkFreshExprMVar (some goalType))
  Lean.Elab.Tactic.appendGoals [x.mvarId!]

example : 0 = 0 := by
  myTactic
  trace_state
  rfl
  exact trivial

[Chris Bailey]

Also straight from the book:

elab "step_1" : tactic => do
  let mvarId ← getMainGoal
  let goalType ← getMainTarget

  let Expr.app (Expr.app (Expr.const `Iff _) a) b := goalType | throwError "Goal type is not of the form `a ↔ b`"

  -- 1. Create new `_`s with appropriate types.
  let mvarId1 ← mkFreshExprMVar (Expr.forallE `xxx a b .default) (userName := "red")
  let mvarId2 ← mkFreshExprMVar (Expr.forallE `yyy b a .default) (userName := "blue")

  -- 2. Assign the main goal to the expression `Iff.intro _ _`.
  mvarId.assign (mkAppN (Expr.const `Iff.intro []) #[a, b, mvarId1, mvarId2])

  -- 3. Report the new `_`s to Lean as the new goals.
  modify fun _ => { goals := [mvarId1.mvarId!, mvarId2.mvarId!] }