Zulip Chat Archive

Stream: general

Topic: coe mv_polynomial

Johan Commelin (Jun 19 2019 at 08:28):

Why is C not a coercion α → mv_polynomial σ α? Is this somehow a bad coercion?

Mario Carneiro (Jun 19 2019 at 08:42):

These coercions are possible but limited in scope

Mario Carneiro (Jun 19 2019 at 08:43):

you have to use has_coe_t

Mario Carneiro (Jun 19 2019 at 08:43):

Also, aren't the terms big enough already? using coe will only make them bigger

Johan Commelin (Jun 19 2019 at 08:45):

That's true. But now we have ↑n : mv_polynomial _ α for n : ℕ and also C (n : α).

Johan Commelin (Jun 19 2019 at 08:46):

Maybe we can still tag the relevant lemmas with norm_cast even if it is not a coe?

Johan Commelin (Jun 19 2019 at 08:46):

It would be nice to normalise these things. I don't yet know what the normal form should be.

Mario Carneiro (Jun 19 2019 at 08:49):

those two are not comparable - you need a lemma to connect them

Mario Carneiro (Jun 19 2019 at 08:50):

I guess I would simp C ↑n = ↑n and possibly use this backwards sometimes

Johan Commelin (Jun 19 2019 at 08:54):

Ok, thanks

Last updated: Dec 20 2023 at 11:08 UTC