panic in Lean.Meta.getEqnsFor

Stream: metaprogramming / tactics

[Chase Norman]

Here is a MWE:

import Mathlib.Data.Int.Basic
#eval (do
  dbg_trace ← Lean.Meta.getEqnsFor? `Int.negOfNat.match_1
)
/-
PANIC at _private.Lean.Environment.0.Lean.AsyncConsts.add Lean.Environment:443:4:
duplicate normalized declaration name Int.negOfNat.match_1.eq_1 vs.
_private.Results.Robustness.0.Int.negOfNat.match_1.eq_1
-/

[Robin Arnez]

That's not what you're supposed to do (you're essentially asking it to look into the definition of the match statement and figure stuff out from there!) You're probably looking for docs#Lean.Meta.Match.getEquationsFor

[Chase Norman]

Is this the only case of a constant that would panic? I’m calling this function on the const symbols in an Expr, so it could be a match, but usually isn’t.

[Robin Arnez]

I think so..? You can test whether to use Lean.Meta.getEqnsFor? or Lean.Meta.Match.getEquationsFor? via Lean.Meta.isMatcher