Commit 2023-09-11 13:37 f48d0465

View on Github →

chore: further cleanup of norm_num (#7046) The main change here is to split NormNum.Core into NormNum.Result and NormNum.Core. Other than that split it is just moving small declarations to better homes.

Estimated changes

added def Lean.Expr.int?
added def Lean.Expr.nat?
added def Lean.Expr.rat?
deleted def Int.rawCast
deleted def Lean.Expr.intLit!
deleted structure Mathlib.Meta.NormNum.IsInt
deleted structure Mathlib.Meta.NormNum.IsNat
deleted inductive Mathlib.Meta.NormNum.IsRat
deleted inductive Mathlib.Meta.NormNum.Result'
deleted def Nat.rawCast
deleted def Rat.rawCast
added def Int.rawCast
added def Nat.rawCast
added def Rat.rawCast