About half of the mathlib3 norm_num test file currently doesn't work, including examples like
example {α} [DivisionRing α] [CharZero α] : (-1:α) ≠ 2 := by norm_numMy understanding (cc @digama0 ?) is that the required norm_num functionality can only be implemented once the port reaches Data.Rat.Cast. This is a placeholder issue just to record this.
About half of the mathlib3
norm_numtest file currently doesn't work, including examples likeMy understanding (cc @digama0 ?) is that the required
norm_numfunctionality can only be implemented once the port reachesData.Rat.Cast. This is a placeholder issue just to record this.