LeanPool.FormalizationOfBoundedArithmetic.Register

Imported Lean Pool material for LeanPool.FormalizationOfBoundedArithmetic.Register.

def Parser.Attr.delta0_simps : Lean.ParserDescr

Simp set used by the bounded-arithmetic import for formula normalization.

Equations

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

def Parser.Attr.delta0_simps_proc : Lean.ParserDescr

Simplification procedure

Equations

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