Zulip Chat Archive
Stream: new members
Topic: make a goal during elaboration
louq (Oct 05 2024 at 18:36):
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 (Oct 06 2024 at 02:26):
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 (Oct 06 2024 at 02:28):
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!] }
Last updated: May 02 2025 at 03:31 UTC