Isabelle自定义action数据类型语法翻译定义报错如何解决？

1. 变量匹配不符合双向翻译要求：你使用了双向翻译符号⇌，Isabelle要求双向翻译规则的左右两侧自由变量必须完全对应，不能有单侧独有的变量。你目前的代码有两处不满足：
   • 左侧接收的第三个参数c没有在右侧用到，你误把bool参数的位置写死成了Some True
   • action类型自带的泛型参数'a，你在右侧给对应位置填了None，这个'a类型变量没有出现在左侧参数中，属于右侧独有未绑定变量
2. 语法模式书写错误：你把优先级参数误写到了模式字符串开头，多了一个多余的3，会导致输入example(...)无法匹配到你定义的语法规则。

如果你只需要把example(...)作为单向语法糖使用，不需要把已有的Action项反向解析回example(...)的写法，优先使用单向翻译符=>，不需要处理反向匹配的变量问题，修改后代码如下：

syntax
  "_example" :: "[int, int, bool] ⇒ 'a action" ("example'(_, _, _')" [60, 60, 60] 60)
translations
  "_example a b c"  => "CONST Action ''example'' (Some a) (Some b) None (Some c) None"

如果你确实需要双向翻译支持，需要补全变量对应关系，给固定的None加类型标注固定泛型参数，避免未绑定变量问题：

syntax
  "_example" :: "[int, int, bool] ⇒ unit action" ("example'(_, _, _')" [60, 60, 60] 60)
translations
  "_example a b c"  ⇌ "CONST Action ''example'' (Some a) (Some b) (None :: unit option) (Some c) None"

修改后输入example(3, 4, True)就会自动翻译为你需要的Action ''example'' (Some 3) (Some 4) None (Some True) None。

内容的提问来源于stack exchange，提问作者Kookie