Zulip Chat Archive

Stream: new members

Topic: Equality of inductive type variants


view this post on Zulip Spencer Killen (May 28 2020 at 17:36):

Given

inductive Choices
| A
| B
open Choices

is it possible to prove

example (h : A = B) : false := sorry

Without introducing new axioms?

view this post on Zulip Spencer Killen (May 28 2020 at 17:37):

Nothing opposed to adding the axioms if I need them, I just don't want to if I don't need to and there's something I'm not understanding about inductive types

view this post on Zulip Johan Commelin (May 28 2020 at 17:38):

Choices.no_confusion

view this post on Zulip Reid Barton (May 28 2020 at 17:52):

Also see https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/

view this post on Zulip Pedro Minicz (May 28 2020 at 23:04):

Reid Barton said:

Also see https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/

Aptly named.


Last updated: May 08 2021 at 03:17 UTC