functional-programming - 如何在 Isabelle 中定义 if then else 表达式？

Question

它向我抱怨我有一个解析错误，但我在手册中找不到正确的语法应该是什么......

  | "my_function x b (Cons3 y) = if x=y then b else (Cons3 y)"

错误：

Inner syntax error⌂
Failed to parse prop

Answer 1

你需要括号：

  | "my_function x b (Cons3 y) = (if x=y then b else (Cons3 y) )"

由于某些原因。

找到一个示例并从该资源中复制它：

https://isabelle.in.tum.de/doc/functions.pdf

Answer 2

在 HOL 对象逻辑中if-then-else，case、 和let构造的优先级与量词一样低，这在大多数其他操作的上下文中需要额外的括号。请查看https://isabelle.in.tum.de/dist/Isabelle2019/doc/logics.pdf，第 10 页。