F *

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）：

因为它的使用是很奇怪的精神分裂症“不透明”限定符被弃用。有两种重载的用途： （1）给定'不透明的val f：t'，行为是将'f'的定义排除在SMT解算器之外。这大致对应于新的“不可约”限定符。 （2）给定'不透明类型t = t'，其行为是为SMT解算器提供't'的定义，但不要内联它，除非统一需要。这大致对应于'unfoldable'（目前是默认值）的行为。