inductively define the type of terms of a signature

Stream: new members

[Andy Ye]

Hi all! New to the stream here. I'm wondering how to inductively define the type of terms with a given signature.
First we have variables:

inductive Var : Type
| var : ℕ → Var

We then define the type class of signatures of function symbols:

@[class] structure Fsym (α : Type) : Type :=
(far : α → ℕ)

However, here comes the tricky part I do not know how to solve. The problem is that, since different function symbols could have different signature, it is not intuitively clear how to inductively define the type of terms with a given signature. What I did is to first define a type function

def nprod : ℕ → Type → Type
| 0     α := unit
| 1     α := α
| (n+1) α := α × (nprod n α)

and proceed to write something as follows:

inductive Term (func : Type) [Fsym func] : Type
| vst : Var → Term
| tap (f : func) (vecx : nprod (Fsym.far f) Term) : Term

However, Lean complaints with error: "inductive type being declared can only be nested inside the parameters of other inductive types". It seems we cannot have a dependent type in the field of inductive definition. I'm not sure whether such type of things have a standard solution or not; I'd really appreciate it if someone could help me with a reasonable definition.

[Eric Wieser]

It's not your problem, but your nprod has two branches that match n=1

[Eric Wieser]

Your problem is that your nprod amounts to using a recursor in an argument of an inductive type, which is not allowed. This produces the same error, inlining nprod:

inductive Term (func : Type*) [Fsym func] : Type
| vst : Var → Term
| tap (f : func) (vecx : (nat.rec_on (Fsym.far f) unit (λ n t, t × Term) : Type*)) : Term

[Eric Wieser]

An easy way out is to use:

inductive Term (func : Type*) [Fsym func] : Type
| vst : Var → Term
| tap (f : func) (vecx : fin (Fsym.far f) → Term) : Term

instead