Zulip Chat Archive

Stream: general

Topic: injections


view this post on Zulip Johan Commelin (Sep 17 2019 at 07:52):

I learnt from #1453 about the existence of an injections tactic. What does it do? Should it be documented?

view this post on Zulip Mario Carneiro (Sep 17 2019 at 07:53):

it's basically repeat {injection}, casing on everything in the context

view this post on Zulip Johan Commelin (Sep 17 2019 at 07:55):

Aha, what does injection do? Should it be documented?

view this post on Zulip Chris Hughes (Sep 17 2019 at 08:01):

It basically just proves that constructors to inductive types are injective. So I can use it to prove x = y and l1 = l2 from x::l1 = y::l2

view this post on Zulip Kevin Buzzard (Sep 17 2019 at 18:06):

I only learnt about this tactic a week or two ago as well.


Last updated: May 14 2021 at 23:14 UTC