Registration for the LDT-local simplifier set

This tiny module declares the opt-in ldt_simp simp set. Lemmas are registered in downstream modules, rather than here, because Lean cannot reliably use a simp attribute in the same file that registers it.

def Parser.Attr.ldt_simp_proc : Lean.ParserDescr

Simplification procedure

Equations

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

def Parser.Attr.ldt_simp : Lean.ParserDescr

Opt-in simplification set for stable LDT proof boilerplate.

Equations

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