Internal simp attribute for zify tactic

ink

def Parser.Attr.zify_simps : Lean.ParserDescr

The simpset zify_simps is used by the tactic zify to moved expression from ℕ to ℤ which gives a well-behaved subtraction.

Equations

• One or more equations did not get rendered due to their size.