Commit 2022-10-13 02:35 458330ed

View on Github →

feat: add simp frontend for norm_num (#451) No new functionality here except that norm_num now calls itself as discharger. More to come.

Estimated changes

Modified Mathlib/Tactic/NormNum.lean

deleted def Lean.Meta.NormNum.derive

deleted def Lean.Meta.NormNum.elabNormNum

deleted def Lean.Meta.NormNum.eval

deleted def Lean.Meta.NormNum.evalEq

deleted theorem Lean.Meta.NormNum.eval_eq_of_isNat

deleted theorem Lean.Meta.NormNum.eval_of_isNat

deleted def Lean.Meta.NormNum.instSemiringNat

deleted def Lean.Meta.NormNum.isNat

deleted theorem Lean.Meta.NormNum.isNat_add

deleted theorem Lean.Meta.NormNum.isNat_cast

deleted theorem Lean.Meta.NormNum.isNat_mul

deleted theorem Lean.Meta.NormNum.isNat_pow

deleted theorem Lean.Meta.NormNum.isNat_rawNat

deleted def Lean.Meta.NormNum.normNumHyp

deleted def Lean.Meta.NormNum.normNumTarget

added def Lean.Meta.Simp.Result.ofTrue

added def Mathlib.Meta.NormNum.elabNormNum

added def Mathlib.Meta.NormNum.eval

added theorem Mathlib.Meta.NormNum.eval_eq_of_isNat

added theorem Mathlib.Meta.NormNum.eval_of_isNat

added def Mathlib.Meta.NormNum.instSemiringNat

added def Mathlib.Meta.NormNum.isNat

added theorem Mathlib.Meta.NormNum.isNat_add

added theorem Mathlib.Meta.NormNum.isNat_cast

added theorem Mathlib.Meta.NormNum.isNat_mul

added theorem Mathlib.Meta.NormNum.isNat_pow

added theorem Mathlib.Meta.NormNum.isNat_rawNat

added def Mathlib.Meta.NormNum.normNumAt

added def Mathlib.Meta.NormNum.tryNormNum?

Modified Mathlib/Tactic/Ring.lean

added structure Mathlib.Tactic.Ring.Cache

added def Mathlib.Tactic.Ring.HornerExpr.e

added def Mathlib.Tactic.Ring.HornerExpr.isZero

added def Mathlib.Tactic.Ring.HornerExpr.pp

added def Mathlib.Tactic.Ring.HornerExpr.reflConv

added def Mathlib.Tactic.Ring.HornerExpr.xadd'

added inductive Mathlib.Tactic.Ring.HornerExpr

added def Mathlib.Tactic.Ring.RingM.run

added def Mathlib.Tactic.Ring.State.numAtoms

added structure Mathlib.Tactic.Ring.State

added def Mathlib.Tactic.Ring.addAtom

added theorem Mathlib.Tactic.Ring.const_add_horner

added def Mathlib.Tactic.Ring.evalAtom

added def Mathlib.Tactic.Ring.evalConstMul

added def Mathlib.Tactic.Ring.evalHorner

added def Mathlib.Tactic.Ring.horner

added theorem Mathlib.Tactic.Ring.horner_add_const

added theorem Mathlib.Tactic.Ring.horner_add_horner_eq

added theorem Mathlib.Tactic.Ring.horner_add_horner_gt

added theorem Mathlib.Tactic.Ring.horner_add_horner_lt

added theorem Mathlib.Tactic.Ring.horner_atom

added theorem Mathlib.Tactic.Ring.horner_const_mul

added theorem Mathlib.Tactic.Ring.horner_horner

added theorem Mathlib.Tactic.Ring.horner_mul_const

added theorem Mathlib.Tactic.Ring.horner_mul_horner

added theorem Mathlib.Tactic.Ring.horner_mul_horner_zero

added theorem Mathlib.Tactic.Ring.horner_pow

added def Mathlib.Tactic.Ring.mkAppCS

added theorem Mathlib.Tactic.Ring.pow_succ_eq

added theorem Mathlib.Tactic.Ring.subst_into_add

added theorem Mathlib.Tactic.Ring.subst_into_mul

added theorem Mathlib.Tactic.Ring.subst_into_pow

added theorem Mathlib.Tactic.Ring.zero_horner

deleted structure Tactic.Ring.Cache

deleted def Tactic.Ring.HornerExpr.e

deleted def Tactic.Ring.HornerExpr.isZero

deleted def Tactic.Ring.HornerExpr.pp

deleted def Tactic.Ring.HornerExpr.reflConv

deleted def Tactic.Ring.HornerExpr.xadd'

deleted inductive Tactic.Ring.HornerExpr

deleted def Tactic.Ring.RingM.run

deleted def Tactic.Ring.State.numAtoms

deleted structure Tactic.Ring.State

deleted def Tactic.Ring.addAtom

deleted theorem Tactic.Ring.const_add_horner

deleted def Tactic.Ring.evalAtom

deleted def Tactic.Ring.evalConstMul

deleted def Tactic.Ring.evalHorner

deleted def Tactic.Ring.horner

deleted theorem Tactic.Ring.horner_add_const

deleted theorem Tactic.Ring.horner_add_horner_eq

deleted theorem Tactic.Ring.horner_add_horner_gt

deleted theorem Tactic.Ring.horner_add_horner_lt

deleted theorem Tactic.Ring.horner_atom

deleted theorem Tactic.Ring.horner_const_mul

deleted theorem Tactic.Ring.horner_horner

deleted theorem Tactic.Ring.horner_mul_const

deleted theorem Tactic.Ring.horner_mul_horner

deleted theorem Tactic.Ring.horner_mul_horner_zero

deleted theorem Tactic.Ring.horner_pow

deleted def Tactic.Ring.mkAppCS

deleted theorem Tactic.Ring.pow_succ_eq

deleted theorem Tactic.Ring.subst_into_add

deleted theorem Tactic.Ring.subst_into_mul

deleted theorem Tactic.Ring.subst_into_pow

deleted theorem Tactic.Ring.zero_horner

Modified scripts/nolints.json