norm_cast bug

Stream: general

[Johan Commelin]

Is this a norm_cast bug?

example (n : ℕ) : @eq.{1} int
  (@coe.{1 1} nat int (@coe_to_lift.{1 1} nat int
    (@coe_base.{1 1} nat int int.has_coe)) n)
  (@coe.{1 1} nat int (@coe_to_lift.{1 1} nat int
    (@nat.cast_coe.{0} int
          (@mul_zero_class.to_has_zero.{0} int (@semiring.to_mul_zero_class.{0} int int.semiring))
          (@monoid.to_has_one.{0} int (@semiring.to_monoid.{0} int int.semiring))
          (@distrib.to_has_add.{0} int (@semiring.to_distrib.{0} int int.semiring)))) n) :=
begin
  norm_cast, -- fails
end

[Johan Commelin]

Try this: simp only [int.nat_cast_eq_coe_nat]

[Johan Commelin]

norm_num should be able to do that, right?

[Kevin Buzzard]

Attempting to tag nat_cast_eq_coe_nat with norm_cast gives norm_cast: badly shaped lemma, rhs can't start with coe