intro タクティク自作例

[Seasawher]

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

[Seasawher]

識別子を引数に持つように変更

elab "my_intro" h:ident : 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 h.getId 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 hA
  exact hq

example : Nat → Nat := by
  my_intro hA
  exact 0