我正在尝试学习伊莎贝尔的布景构建,但我失败了。 假设您需要一个函数来给出所有小于给定数字的自然数。我认为这应该有效:
fun set_of_nats ::"'nat ⇒'nat set" where
"set_of_nats b = {a |(a::nat). a < b}"
但事实并非如此。错误:
Type unification failed: Variable 'nat::type not of sort ord
Type error in application: incompatible operand type
Operator: (<) a :: ??'a ⇒ bool
Operand: b :: 'nat
当我不动态构造集合而是给它一个固定条件时,也会发生同样的错误,例如用任何 nat 替换
b
,如 5
。错误仍然相同。
我在这里做错了什么?在这种情况下,伊莎贝尔如何处理潜在的无限集(想象一下比较不是小于而是更大)
您应该写
nat
而不是 'nat
。 '
表示这是一个类型变量,即任意类型。