Isabelle 的集合运算符 (') :: ('a => 'b) => 'a => 'b 集合中的主要符号是什么？
What is the main symbol in Isabelle's set operator (‘) :: ('a => 'b) => 'a set => 'b set?
我想知道下面伊莎贝尔教程 main.pdf 中的符号 ‘ 是什么（在“设置”部分下）？
(‘) :: ('a => 'b) => 'a set => 'b set
通过查看符号选项卡，我能找到形状最接近的是“未排序”类别下的 \<acute>。我试图评估以下表达式，但它没有解析：
value "´ (λ(n::nat). n+1) {1,2}"
value "(λ(n::nat). n+1) ´ {1,2}"
谁能帮忙解释一下这里的用法和作用？
我认为您要查找的符号是 `，而不是 ‘ 或 ´。符号 ` 是常量 image 的中缀符号，在 Isabelle/HOL 的主库中理论上定义了 Set.thy。希望常量的名称是不言自明的。为了完整起见，我重申这个答案中的定义：
definition image :: "('a ⇒ 'b) ⇒ 'a set ⇒ 'b set" (infixr "`" 90)
where "f ` A = {y. ∃x∈A. y = f x}"
因此，
value "(λ(n::nat). n+1) ` {1,2}"
如预期的那样评估为 "{2, 3}" :: "nat set"。
我想知道下面伊莎贝尔教程 main.pdf 中的符号 ‘ 是什么（在“设置”部分下）？
(‘) :: ('a => 'b) => 'a set => 'b set
通过查看符号选项卡，我能找到形状最接近的是“未排序”类别下的 \<acute>。我试图评估以下表达式，但它没有解析：
value "´ (λ(n::nat). n+1) {1,2}"
value "(λ(n::nat). n+1) ´ {1,2}"
谁能帮忙解释一下这里的用法和作用？
我认为您要查找的符号是 `，而不是 ‘ 或 ´。符号 ` 是常量 image 的中缀符号，在 Isabelle/HOL 的主库中理论上定义了 Set.thy。希望常量的名称是不言自明的。为了完整起见，我重申这个答案中的定义：
definition image :: "('a ⇒ 'b) ⇒ 'a set ⇒ 'b set" (infixr "`" 90)
where "f ` A = {y. ∃x∈A. y = f x}"
因此，
value "(λ(n::nat). n+1) ` {1,2}"
如预期的那样评估为 "{2, 3}" :: "nat set"。