failed to define inductive datatype

Stream: new members

[Pedro Minicz]

Why definitions term₂ and term₃ don't work? I don't understand the "nested occurrence [...]" error messages. Is there any work around I can do to fix them?

structure Language :=
(functions : ℕ → Type)
(relations : ℕ → Type)

variable (L : Language)

def Language.constants := L.functions 0

inductive term₁
| var (k : ℕ) : term₁
| func {l : ℕ} (f : L.functions l) (args : list term₁) : term₁

-- nested occurrence contains variables that are not parameters
inductive term₂
| var (k : ℕ) : term₂
| func {l : ℕ} (f : L.functions l) (args : vector term₂ l) : term₂

-- nested occurrence lives in universe '0' but must live in resultant universe '1'
inductive term₃
| var (k : ℕ) : term₃
| func {l : ℕ} (f : L.functions l) (args : list term₃) (h : args.length = l): term₃

[Reid Barton]

I suggest using args : fin l → term.

[Pedro Minicz]

Thanks for the suggestion.

[Pedro Minicz]

I would love to hear an explanation of why definitions 2 and 3 don't work tho.

[Alex J. Best]

Check out https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/nested.20inductive.20type.20error/near/211030307

[Pedro Minicz]

Thanks Alex :smiley: