Why sometime no no_confusion?

Stream: new members

[Andre Kuhlenschmidt]

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

[Mario Carneiro]

It's a nested inductive

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Andre Kuhlenschmidt]

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.