问题描述
我对 Isabelle 还很陌生，我在打字时遇到了一些麻烦：我想要两个独立但重叠的类型，比如“a”和“b”。将它们视为集合，我希望将 'b = 'a \cup {tau} 用于未出现在 'a 中的特定 tau。据我了解，您可以在 Isabelle 中使用“fixes tau :: 'a”扩展类型，但似乎原始类型 'a （没有 tau）丢失了： Current Isabelle code using fixes
我在以后的公式中需要这两种类型，那么有没有办法在将 tau 固定到它之前“保存”'a 的状态？
任何帮助将不胜感激！
解决方法
您误解了语言环境。修复引入了某种类型的常量。记住语言环境的含义：
locale t =
fixes x
assumes "P x"
begin
lemma b: Q
sorry
表示“!!x。P x ==> Q”。您没有扩展类型。
关于实际问题：您不能直接扩展类型或直接在 HOL 中表达。这是不可能的。在实践中扩展类型有两种解决方案：
- 一种数据类型
datatype 'a myunion = Either1 'a | Tau。在这种情况下，它实际上与'a option同构。 - 联合类型（参见 here for another SO question on the topic）