nested inductive type

Stream: general

[Björn Fischer]

Is it possible to define a nested inductive type on a vector-like structure instead of lists?

inductive expression : Type
| a {dim : ℕ} (idx : vector (expression) dim) /- omitted constraints on dim -/ : expression
| b : expression

I get the following error: nested occurrence [...] contains variables that are not parameters.

[Chris Hughes]

I think this is an inductive recursive type, since it depends on the length function for lists. I don't think this is possible.

[Mario Carneiro]

This isn't an inductive recursive, but it's not a supported nested inductive. The easiest solution is to use fin dim -> expression instead of vector expression dim

[Björn Fischer]

That works. Thanks!

[Björn Fischer]

Follow up question:
If I want to define a recursive function over expressions like so:

def f : expression -> N
| (a idx) := 1 + ((vector.of_fn idx).map f).sum
| b ...
using_well_founded {rel_tac := λ_ _, `[exact ⟨_, measure_wf (λ e, expression_size e)⟩] }

I have to proof that the function application is decreasing for some arbitrary expression e, i.e. expression_size e < expression_size (a idx). However I don't have a proof that e comes from idx, ergo I cannot proof it.
The only way around that I can think of is to use the recursor directly. Is there a more convenient way?
(I left out some details, expression is actually indexed over types)

[Chris Hughes]

This is probably easier to define using expression.rec_on

def f (e : expression) : ℕ :=
expression.rec_on e
  (λ n idx f,  (vector.of_fn f).1.sum + 1)
  _