# Zulip Chat Archive

## Stream: general

### Topic: nested inductive type

#### Björn Fischer (Apr 29 2019 at 09:17):

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 (Apr 29 2019 at 09:21):

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 (Apr 29 2019 at 09:33):

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 (Apr 29 2019 at 11:21):

That works. Thanks!

#### Björn Fischer (May 14 2019 at 13:49):

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 (May 14 2019 at 15:30):

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) _

Last updated: May 10 2021 at 16:20 UTC