Metaprogramming tutorial: custom assumption

Stream: lean4

[Hanting Zhang]

I was trying to follow the tactic chapter when I ran across this issue:

import Lean

elab "myAssump" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let goal ← Lean.Elab.Tactic.getMainGoal
    let goalDecl ← Lean.Meta.getMVarDecl goal
    let goalType := goalDecl.type
    let ctx ← Lean.MonadLCtx.getLCtx -- get the local context.
    let hyp? ← ctx.findDeclM? fun decl => do
      let declExpr := decl.toExpr
      let declType ← Lean.Meta.inferType declExpr
      if ← Lean.Meta.isExprDefEq declType goalType
        then return some declExpr
        else return none
    match hyp? with
    | some expr => Lean.Elab.Tactic.closeMainGoal expr
    | none =>
      Lean.Meta.throwTacticEx `assump goal
        (m!"unable to find matching hypothesis of type ({goalType})")

def foo : 3 = 3 := by
  myAssump

It throws an error saying:

fail to show termination for
  foo
with errors
structural recursion cannot be used

[Hanting Zhang]

Why is structural recursion showing up? I also don't really know how I'm approach debugging in the tactic framework yet. What are the trace options that would give me the information to debug these kinds of errors?

Thanks!

[Alexander Bentkamp]

You can insert trace[Elab.debug] "{declExpr}" above the if in your code. And you'll need to set set_option trace.Elab.debug true above the def to see the debug output. Then you'll see that foo itself is in the list of local declarations, which can be used for recursion.

[Alexander Bentkamp]

You can exclude this recursive declaration by checking decl.isAuxDecl.

[Hanting Zhang]

Oh I see now! Adding decl.isAuxDecl fixes it indeed. Thanks for the trace tips as well!