伊莎贝尔：Wellsortedness错误

该value命令在内部使用代码生成器进行评估，并且代码生成器会产生分类错误。在上述情况下，伊莎贝尔（Isabelle）的类型检查器会推导带有该术语的类型变量的类型mirror Typ，即'a tree类型变量'a具有sort的位置type。由于a'a tree可能包含的值'a，因此代码生成器还会尝试生成用于漂亮打印的代码，该代码'a tree在type类中实现term_of。但是，这失败了，因为for的推断类型'a是typeand not term_of，这就是错误排序错误的原因。

避免错误的最简单方法是显式地指定单态类型。例如，

value "mirror Tip :: nat tree"

应该管用。