Zulip Chat Archive

Stream: lean4

Topic: Show constructors are injective and non-overlapping

Erika Su (Dec 27 2022 at 04:40):

What's the primitives provided by lean that can show constructors are non-overlapping and injective?
Also, what's the use of noConfustionType?

Notification Bot (Dec 27 2022 at 04:51):

Erika Su has marked this topic as resolved.

Notification Bot (Dec 27 2022 at 04:51):

Erika Su has marked this topic as unresolved.

Kevin Buzzard (Dec 27 2022 at 05:49):

Here's a basic description of what no_confusion is doing in lean 3: https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/

Last updated: Dec 20 2023 at 11:08 UTC