types - 假设 F* 中的 val 和 opaque 类型构造

Question

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

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

assume val name: type

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

opaque type name (...) ...

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

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

Answer 1

的意思assume val name : Type是假设存在一个公理Type，它可以被 访问name。由于它是一个公理，因此它不会有实现，并且如果被滥用（例如通过假设一个严格小于 0 的自然数）可能会导致逻辑不一致。

F* 教程与去年发生的多项更改并不完全同步，并且opaque是该问题的一个实例。从编译器源代码（截至写作时，在src/tosyntax/FStar.ToSyntax.fs）：

'opaque' 限定词已被弃用，因为它的使用令人奇怪地精神分裂。有两种重载用途：(1) 给定“不透明 val f : t”，行为是将“f”的定义排除在 SMT 求解器中。这大致对应于新的“不可约”限定词。(2) 给定“不透明类型 t = t”，行为是向 SMT 求解器提供“t”的定义，而不是内联它，除非绝对需要统一。这大致对应于“unfoldable”的行为（目前是默认设置）。