问题标签 [fstar]

我正在尝试在最新的 Ubuntu 和单声道上编译 FStar 语言。GitHub repo提供了一些构建指令，但它对我不起作用。后

我收到此错误消息：

完整日志可在此处获取。

如何在单声道上构建 FStar 语言？

F*教程的第9章有一个例子：

有人可以在这里解释这个符号吗？我知道这WP是前置条件和P后置条件，但什么是P b？应用于b?的后置条件

我刚从 F* 开始，我的意思是我已经写了几行连同教程。到目前为止，这真的很有趣，我想继续学习。

我自己尝试做的第一件事是编写一个表示非空列表的类型。这是我的尝试：

但我得到了错误

无法验证隐式参数：子类型检查失败；预期类型 (a#6468:Type{(hasEq a@0)}); 得到类型类型

我知道我走在正确的轨道上，因为如果我将列表类型限制为包含字符串，这确实有效：

我假设这意味着l <> []在原始示例中无效，因为我没有指定'a应该支持平等。问题是我一生都无法弄清楚如何做到这一点。我猜这与更高的类型hasEq有关，但尝试诸如：

没有把我带到任何地方。该教程没有涵盖hasEq，我在 GitHub 存储库中的示例中找不到任何有用的东西，所以现在我被困住了。

我是 F* 的新手，虽然教程写得很好，但我缺少一些好的 API 页面供参考。

所以我需要以下构造的确切含义：

我会说这条线将正在使用的名称注册到求解器中？

调用类型不透明的效果是什么？它可能需要的参数列表呢？

请包括您可能用来给出此答案的参考资料。

他们来自微软，似乎他们是证明助理？除了语法上的差异之外，还有哪些实际方面使它们彼此不同（比如自动化能力、表达能力等）？我是形式验证的新手。

编辑：我不是在问哪个更好，我只是对这些工具提供的不同功能之间的技术比较感兴趣。我正在寻找这样的东西

我刚刚开始学习 F*，正在阅读教程。其中一项练习是证明reverse列表上的函数是单射的。因为这是从对合是单射的事实得出的，所以我想将该事实表达为 F* 中的一个引理。为此，我定义

这是f在 F* 中定义内合或内射概念的正确方法吗？

然后我陈述引理

非正式地，证明可以写成

我如何在 F* 中表达这样的证明？一般来说，可以使用哪些 F* 语言结构来证明以下形式的语句，类型的谓词在forall (x:a). phi x哪里？phia

根据关于子结构类型系统的维基百科文章，F* 支持某种线性类型。这是真的？如果是这样，怎么做？我在 F* 教程中找不到任何有关它的信息。

作为尝试熟悉 F* 的实验，我尝试实现一个应用函子。我陷入了一个看起来很奇怪的类型检查错误。我还不确定这是否是由于我不知道的类型检查中的某些功能/逻辑，或者这是否是由真正的错误引起的。

这是给我带来麻烦的代码部分：

这是相应的错误：

有人可以向我指出我缺少什么吗？类型统一的行为是否受子类型化的影响？还是应该进行类型检查，这是编译器错误？

正如我们所知，我们在 Agda（ Emacs 中的Ctrl+ c Ctrl+ a）以及 Idris 和 Coq 中都有“自动”（证明搜索），但是当我深入研究 F* 的 Emacs 模式时，我没有找到类似的功能.

F*有这个功能吗？如果是这样，我该如何使用它？

https://github.com/FStarLang/FStar/wiki/Profiling-Z3-queries的 wiki 页面建议使用 Z3 Axiom Profiler；但是，Z3 Axiom Profiler 似乎只能在 Windows 上可靠地工作。

在没有 Z3 Axiom Profiler 的情况下，如何轻松获得最触发的量词？