Zulip Chat Archive
Stream: lean4
Topic: injectivity of inductive constructors
Yakov Pechersky (Apr 30 2021 at 15:19):
What's the lean4 equivalent of the auto-generated inductive_type.constructor.inj lemmas?
Mario Carneiro (Apr 30 2021 at 15:23):
noConfusion
Last updated: Dec 20 2023 at 11:08 UTC