CODEWITHSUNDEEP
functional-programmingisabelletheorem-provinghol
Charlie Parker
Charlie Parker

Reputation: 5199

How does one define a if then else expression in Isabelle?

It complains to me I have a parsing error but I can't find in the manual what the right syntax is suppose to be...

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

error:


Inner syntax error⌂
Failed to parse prop

Upvotes: 1

Views: 915

Answers (2)

Javier Díaz
Javier Díaz

Reputation: 1101

In the HOL object logic, the if-then-else, case, and let constructs have as low a precedence as quantifiers, which requires additional enclosing parentheses in the context of most other operations. Please have a look at https://isabelle.in.tum.de/dist/Isabelle2019/doc/logics.pdf, page 10.

Upvotes: 2

Charlie Parker
Charlie Parker

Reputation: 5199

You need brackets:

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

for some reason.

Found an example and copied it from this resource:

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

Upvotes: 2

Related Questions