のvalとopaque型の構造体を前提としています。私はF *を初めて使用していますが、このチュートリアルはよく書かれていますが、参照できるようにいくつかの良いAPIページがありません。F *
だから私は、次の構成のための正確な意味を必要とする：
assume val name: type
私はこの行は名前が使用されてソルバーに登録すると言うだろうか？
opaque type name (...) ...
タイプを不透明にする効果は何ですか？それが取るかもしれないパラメタのリストはどうですか？
この回答に使用した参考情報を含めてください。
assume val name : Typeの意味は、nameでアクセスできるTypeの公理を仮定することです。それは公理であるため、実装されず、誤って使用された場合（たとえば、自然数が厳密に0より小さいと仮定して）、論理的な不一致につながる可能性があります。
F *チュートリアルでは、昨年に発生した複数の変更が正確ではなく、opaqueがその問題のインスタンスです。 （src/tosyntax/FStar.ToSyntax.fsへの書き込みなど、）コンパイラのソースから ：
。 （1）「不透明なval f：t」と指定すると、SMTソルバーに 'f'の定義を除外するように動作しました。これは新しい「還元不可能な」修飾子におおよそ対応します。 （2） '不透明型t = t' 'を指定すると、SMTソルバに' t 'の定義を提供することができましたが、統一のために絶対必要でない限り、それをインライン化することはありませんでした。これは、おおまかに「unfoldable」（現在はデフォルト）の動作に対応しています。