Nested inductive type with vector

Stream: new members

[Rui Liu]

Lean seems to allow the following definition even when tree is nested in the list class, as described under https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html#mutual-and-nested-inductive-types

inductive tree (α : Type u)
| mk : α → list tree → tree

However, I can't seem to get this work with vector, the following code doesn't compile:

import data.vector

universe u
inductive tree (α : Type u)
| mk : α → vector tree 2 → tree

Any way to get lean work with vector? Maybe define a custom vector that allows nested inductive definition?

[Yakov Pechersky]

import data.fin

universe u
inductive tree (α : Type u)
| mk : α → (fin 2 → tree) → tree

[Yakov Pechersky]

and then if you really want a vector, you can do vector.of_fn.

[Rui Liu]

@Yakov Pechersky

I don't seem to be able to import data.fin? I'm developing from vscode after downloading the release here https://github.com/leanprover/lean/releases

[Eric Wieser]

That's the old abandoned version of lean

[Rui Liu]

Oh actually if I just don't run import data.fin it also seems to work...

[Rui Liu]

@Eric Wieser What version should I use instead?

[Eric Wieser]

leanprover-community/lean

[Rui Liu]

Oh actually I did download from there https://github.com/leanprover-community/lean/releases/tag/v3.23.0

[Alex J. Best]

Try following the recommended instructions at #install

[Mario Carneiro]

Lean's support for nested inductive types is spotty, and in particular it does not support dependent nested inductives. These inductives are not part of the kernel but are instead simulated by a compilation strategy that doesn't work in the dependent case. Like Yakov says, you should use functions instead, because these are native inductives and have all the nice properties you would expect