由精益類型列表構建的歸納類型

Question

我想定義一個歸納類型，可以從精益本身的列表構建。然而

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屬於它的參數的類型宇宙（除非該參數爲支柱）。所以如果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

精益3現在支持嵌套感性聲明：

inductive a : Type 
| aFromAs : list a → a 

Answer 2

它看起來像Lean doesn't have support for nested datatypes所以你最好的賭注它們編碼爲相互遞歸定義：

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