【发布时间】：2014-10-26 11:52:09
【问题描述】：
Isabelle 中是否有任何用于二叉树的预定义函数？ 例如移动到二叉树的左侧？
【问题讨论】：
标签： binary-tree isabelle
【发布时间】：2014-10-26 11:52:09
【问题描述】：
自 Isabelle2014 以来，~~/src/HOL/Library/Tree 中有一个关于二叉树的小理论。如果此类型符合您的目的，您可以使用它以及在其上定义的功能。例如，有选择器函数 left 和 right 返回树的左右子树。
如果您必须定义自己的数据类型，您可以使用datatype_new 的选择器语法来定义您认为合适的选择器。
【讨论】：