Function is_equation_name 

pub fn is_equation_name(name: &str) -> bool

Whether a name is one this module MINTS, rather than one it generates lemmas for.

This is Lean’s isEqnReservedNameSuffix (Lean/Meta/Eqns.lean:63-66) — the eq_<digits> test — plus the unfold suffix. It is the re-entrancy guard: without it the first lemma generated would ask for its own lemmas, for ever.