type-theory - 由精益中该类型的列表构造的归纳类型

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