如何从 Windows 安装导出 Isabelle 会话？

编程问答 2022-05-17

问题描述

我有简单的理论文件

19895

[Function: getUptime] {
  [Symbol(Symbol.toPrimitive)]: [Function (anonymous)]
}

而且我可以看到我在 jEdit 'Plugins - Isabelle - browse Session information' 中看到我的会话名称是 HOL。所以我试图导出这个会话：

theory Max_Of_Two_Integers_Real
  imports (* Main *)
    "../Imperative_HOL" 
    Subarray
    "HOL-Library.Multiset"
    "HOL-Library.Code_Target_Numeral"
    "HOL-Library.Code_Target_Nat"
    "HOL-Library.Code_Abstract_Nat"
begin

deFinition two_integer_max_case_def :: "nat ⇒ nat ⇒ nat" where
"two_integer_max_case_def a b = (case a > b of True ⇒ a | False ⇒ b)"

deFinition "example_case_def = two_integer_max_case_def 1 2"

export_code example_case_def checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp

end

一般来说，导出是好的——它包含很多标记*文件，这些文件可能是 XML 中抽象语法树的前身。但是没有文件可以归因于我的 Max_Of_Two_Integers_Real。也没有我在自己的理论文件中导入的 HOL_Imperative 文件。

因此 - export 导出了非常大的会话数据，但我的理论文件和导入的理论文件不在导出文件中。我做错了什么？如何要求也从会话中导出我的理论文件？

我的理论文件很简单，虽然有一些错误阻止了代码的生成，但通常我的理论文件是有效的——其中没有公开证明义务，并且在语法上也是正确的。所以 - 它应该已经出口了。

解决方法

暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！

如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。

小编邮箱:dio#foxmail.com (将#修改为@）

isabelle