intro タクティク自作例

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

  let Expr.forallE _ pFrom pTo _ := goalType
    | throwError "Goal type is not of the form `a → b`"

  let handyMvarId ← withLocalDecl `hA BinderInfo.default pFrom (fun fvar => do
    -- 1. Create new `_`s with appropriate types.
    let mvarId1 ← mkFreshExprMVar pTo MetavarKind.syntheticOpaque `goal
    -- 2. Assign the main goal to the expression `fun hA => _`.
    mvarId.assign (← mkLambdaFVars #[fvar] mvarId1)
    -- just a handy way to return a handyRedMvarId for the next code
    return mvarId1.mvarId!
  )
  modify fun _ => { goals := [handyMvarId] }

example {p q : Prop} (hq : q) : p → q := by
  my_intro
  exact hq

example : Nat → Nat := by
  my_intro
  exact 0

No target file or requested change is specified. Start by locating the introductory tactic material in the repository and compare its examples with the supplied snippet; completion should be defined by the issue author, including where the example belongs and how it should be checked.