Equations
- One or more equations did not get rendered due to their size.
Instances For
@[export lean_csimp_replace_constants]
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Compiler.hasCSimpAttribute env declName = (Lean.ScopedEnvExtension.getState Lean.Compiler.CSimp.ext env).thmNames.contains declName