构造 Isabelle 中满足给定条件的所有元素的 Set 的函数

Question

我正在尝试学习伊莎贝尔的布景构建，但我失败了。 假设您需要一个函数来给出所有小于给定数字的自然数。我认为这应该有效：

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

。错误仍然相同。

我在这里做错了什么？在这种情况下，伊莎贝尔如何处理潜在的无限集（想象一下比较不是小于而是更大）

Answer 1

您应该写

nat

而不是

'nat

。

'

表示这是一个类型变量，即任意类型。