Мне жалуется, что у меня ошибка синтаксического анализа, но я не могу найти в руководстве, какой правильный синтаксис должен быть ...
| "my_function x b (Cons3 y) = if x=y then b else (Cons3 y)"
Ошибка:
Inner syntax error⌂ Failed to parse prop
В объектах HOL logi c конструкции if-then-else, case и let имеют меньший приоритет, чем квантификаторы, что требует дополнительных заключающих скобок в контексте большинства других операций. Пожалуйста, посмотрите на https://isabelle.in.tum.de/dist/Isabelle2019/doc/logics.pdf, стр. 10.
if-then-else
case
let
Вам нужны скобки:
| "my_function x b (Cons3 y) = (if x=y then b else (Cons3 y) )"
по некоторым причинам.
Найден пример и скопирован из этого ресурса:
https://isabelle.in.tum.de/doc/functions.pdf