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: May 02 2025 at 03:31 UTC