在Isabelle中如何定义if if 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页。