Zulip Chat Archive

Stream: new members

Topic: Why sometime no no_confusion?


view this post on Zulip Andre Kuhlenschmidt (Mar 04 2019 at 19:52):

Is there a limitation to the derivation of no_confusion theorems?
The following inductive type doesn't generate one:

inductive type
| TVar  : nat → type
| Bool  : type
| Arrow : type → type → type
| TDef  : nat → list type → type

#print prefix type

view this post on Zulip Mario Carneiro (Mar 04 2019 at 20:03):

It's a nested inductive

view this post on Zulip Mario Carneiro (Mar 04 2019 at 20:04):

This is not built in to lean but is compiled, so it has a different set of autogenerated theorems

view this post on Zulip Mario Carneiro (Mar 04 2019 at 20:05):

I generally recommend against using nested inductives at all because the lean support is spotty

view this post on Zulip Mario Carneiro (Mar 04 2019 at 20:06):

(The reason it is a nested inductive is because the last constructor mentions list type, where type is the inductive type under construction)

view this post on Zulip Andre Kuhlenschmidt (Mar 04 2019 at 20:14):

Is the standard way of avoiding list type to make a mutually inductive definition?

mutual inductive type, list_type
with type : Type
| TVar  : nat → type
| Bool  : type
| Arrow : type → type → type
| TDef  : nat → list_type → type
with list_type : Type
| nil : list_type
| cons : type -> list_type -> list_type

#print prefix type

This seems to work.


Last updated: May 13 2021 at 05:21 UTC