Commit 2022-02-24 13:15 042ca5df

View on Github →

feat: norm_cast (#191)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Defs.lean

modified theorem Int.cast_negSucc

modified theorem Int.cast_one

modified theorem Int.cast_zero

modified theorem Nat.cast_add

modified theorem Nat.cast_ofNat

modified theorem Nat.cast_succ

modified theorem Nat.cast_zero

Modified Mathlib/Algebra/Ring/Basic.lean

modified theorem Int.cast_Nat_cast

added theorem Int.cast_eq_cast_iff_Nat

modified theorem Int.cast_id

added theorem Int.natAbs_cast

modified theorem Nat.cast_id

Modified Mathlib/Init/Data/Int/Basic.lean

Modified Mathlib/Init/Data/Int/Order.lean

modified theorem Int.ofNat_le

modified theorem Int.ofNat_lt

Modified Mathlib/Mathport/Syntax.lean

Modified Mathlib/Tactic/NormCast.lean

deleted structure Tactic.NormCast.NormCastExtension

deleted def Tactic.NormCast.addElim

deleted def Tactic.NormCast.addInfer

deleted def Tactic.NormCast.addMove

deleted def Tactic.NormCast.addSquash

Created Mathlib/Tactic/NormCast/CoeExt.lean

added structure Tactic.NormCast.CoeFnInfo

added inductive Tactic.NormCast.CoeFnType

added def Tactic.NormCast.addCoeDelaborator

added def Tactic.NormCast.coeDelaborator

added def Tactic.NormCast.getCoeFnInfo?

added def Tactic.NormCast.registerCoercion

Created Mathlib/Tactic/NormCast/Ext.lean

added inductive Tactic.NormCast.Label

added structure Tactic.NormCast.NormCastExtension

added def Tactic.NormCast.addElim

added def Tactic.NormCast.addInfer

added def Tactic.NormCast.addMove

added def Tactic.NormCast.addSquash

added def Tactic.NormCast.classifyType

added def Tactic.NormCast.countInternalCoes

added def Tactic.NormCast.getSimpArgs

Created Mathlib/Tactic/NormCast/Lemmas.lean

Created Mathlib/Tactic/NormCast/Tactic.lean

added def Tactic.NormCast.derive

added def Tactic.NormCast.evalConvNormCast

added def Tactic.NormCast.evalPushCast

added def Tactic.NormCast.isCoeOf?

added def Tactic.NormCast.isNumeral?

added def Tactic.NormCast.mkCoe

added def Tactic.NormCast.normCastHyp

added def Tactic.NormCast.normCastTarget

added def Tactic.NormCast.numeralToCoe

added def Tactic.NormCast.prove

added def Tactic.NormCast.proveEqUsing

added def Tactic.NormCast.proveEqUsingDown

added def Tactic.NormCast.splittingProcedure

Created Mathlib/Util/Simp.lean

added def Lean.Meta.DiscrTree.getElements

added def Lean.Meta.Simp.getPropHyps

added def Lean.Meta.Simp.mkCast

added def Lean.Meta.Simp.mkEqSymm

added def Lean.Meta.Simp.mkSimpContext'

added def Std.PHashSet.toList

Created test/norm_cast.lean

added theorem b

added def hidden.WithZero.of

added def hidden.WithZero

added theorem hidden.coe_inj

added theorem hidden.coe_one

added theorem hidden.mul_coe

added structure p