Writing Tactics: run tactic on a hypothesis

Stream: lean4

[Anurudh Peduri]

Hey all, I need some help writing a tactic that loops through all the hypotheses and runs some tactic on each of them.

For example, I want to run cases p on every p: Point in my local context.

import Lean.Elab.Tactic

abbrev Point := Int × Int

elab "get_coordinates" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let ctx ← Lean.MonadLCtx.getLCtx
    ctx.forM $ fun (decl: Lean.LocalDecl) => do
      let declExpr := decl.toExpr -- Find the expression of the declaration.
      let declType ← Lean.Meta.inferType declExpr -- Find the type.
      if (← Lean.Meta.isExprDefEq declType (Lean.Expr.const ``Point [])) then
        dbg_trace f!"! Point"
        -- TODO run `cases decl`
    return

How do I do this? I was looking through the metaprogramming-book, but couldn't find how to run a tactic on a decl that I have.

[Kyle Miller]

There's docs#Lean.MVarId.casesRec for doing cases on everything in the local context that satisfies some condition

[Kyle Miller]

Lean.MVarId.substEqs is an example usage of it.

[Kyle Miller]

docs#Lean.Elab.Tactic.liftMetaTactic is useful in place of withMainContext to get the main goal and to be able to replace it with the results of running casesRec

[Anurudh Peduri]

Oh wow, thanks @Kyle Miller! let me try this out.

[Anurudh Peduri]

thank you, it worked. :)