Attributes for representation-independent numerical automation

The attributes are declared separately so numerical families can register semantic and concrete rules without importing the tactic implementation. Semantic rules must be proved equations or equivalences. Concrete reduction rules are used only by the explicit closed-term phase.

def Parser.Attr.numerics_simps_proc : Lean.ParserDescr

Simplification procedure

def Parser.Attr.numerics_simps : Lean.ParserDescr

Representation-independent semantic rewrites used by numerics.

def Parser.Attr.numerics_side : Lean.ParserDescr

Routine finiteness, range, and operation-precondition rewrites used by numerics.

def Parser.Attr.numerics_side_proc : Lean.ParserDescr

Simplification procedure

def Parser.Attr.numerics_reduction : Lean.ParserDescr

Concrete carrier and decoder reductions used by numerics_reduce and numerics!.

def Parser.Attr.numerics_reduction_proc : Lean.ParserDescr

Simplification procedure