Search code examples
type-theorylean

Inductive type constructed by a list of that type in Lean

I would like to define an inductive type that can be constructed from a list of itself in lean. However

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

gives the error:

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

Fine, so I set_option pp.universes true and list belongs to the type universe of its parameter (unless the parameter is Prop). So if a is Type₁ everything should be fine. But

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

gives the error 

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

It looks valid to me. This seams like it should work.

Solution

  • Lean 3 now supports nested inductive declarations:

    inductive a : Type
| aFromAs : list a → a