由精益中的那种类型的列表构成的归纳类型

作者: biu~
发布时间: 2025-02-15 10:07:32 (12天前)
转自：

3 条回复

0#
回复此人
至此 | 2019-08-31 10-32

<div class =“post-text”itemprop =“text”> <P> 看起来像 <a href="https://github.com/leanprover/lean/wiki/Inductive-datatypes#encoding-datatypes-that-contain-recursive-occurrences-nested-in-existing-datatypes" rel="nofollow noreferrer"> 精益不支持嵌套数据类型 </A> 所以你最好把它们编码为相互递归的定义： </p> <pre> <code> inductive a := node : as -> a with as := | nil : as | cons : a -> as -> as </code> </pre> </DIV>

编辑
1#
回复此人
trpnest | 2019-08-31 10-32

<div class =“post-text”itemprop =“text”> <P> 精益3现在支持嵌套的归纳声明： </p> <pre> <code> inductive a : Type | aFromAs : list a �� a </code> </pre> </DIV>

编辑

登录后才能参与评论