Zulip Chat Archive

Stream: general

Topic: norm_cast bug


view this post on Zulip Johan Commelin (May 29 2020 at 14:12):

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

view this post on Zulip Johan Commelin (May 29 2020 at 14:13):

Try this: simp only [int.nat_cast_eq_coe_nat]

view this post on Zulip Johan Commelin (May 29 2020 at 14:14):

norm_num should be able to do that, right?

view this post on Zulip Kevin Buzzard (May 29 2020 at 14:54):

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


Last updated: May 15 2021 at 00:39 UTC