Zulip Chat Archive
Stream: general
Topic: injections
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?
Mario Carneiro (Sep 17 2019 at 07:53):
it's basically repeat {injection}, casing on everything in the context
Johan Commelin (Sep 17 2019 at 07:55):
Aha, what does injection do? Should it be documented?
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
Kevin Buzzard (Sep 17 2019 at 18:06):
I only learnt about this tactic a week or two ago as well.
Last updated: Dec 20 2023 at 11:08 UTC