Индуктивный тип, построенный по списку этого типа в Lean

Question

Я хотел бы определить индуктивный тип, который может быть построен из списка самого себя в Lean. тем не мение

inductive a : Type :=
| aFromAs : list a → a

выдает ошибку:

failed to infer inductive datatype resultant universe, provide the universe levels explicitly

Хорошо, поэтому я set_option pp.universes true а также list принадлежит типу юниверса его параметра (если параметр не является Prop). Так что если a является Type₁ все должно быть хорошо. Но

inductive a : Type₁ :=
| aFromAs : list a → a

выдает ошибку

arg #1 of aFromAs contains an non valid occurrence of the datatype being declared

Это выглядит актуально для меня. Это швы, как это должно работать.

Answer 1

Lean 3 теперь поддерживает вложенные индуктивные объявления:

inductive a : Type
| aFromAs : list a → a

Answer 2

Похоже, что у Lean нет поддержки вложенных типов данных, поэтому лучше всего кодировать их как взаимно рекурсивные определения:

inductive a := node : as -> a
with as :=
   | nil  : as
   | cons : a -> as -> as