2017-12-16 5 views
2

Coq 8.7は一般的なSsreflectライブラリを統合しています。そのライブラリは、したがって、次のようにインポートすることができます。ssrnatはCoq 8.7に含まれていますか?

From Coq Require Import ssreflect ssrfun ssrbool. 

しかし、私はssrnatをインポートしようとすると、それはそれはUnable to locate library ssrnat with prefix Coqだと文句を言い、私はどちらかのディスク上のCoqの分布のssrnatを見つけることができません。 ssrnatは何らかの理由で意図的に含まれていなかったか、別のモジュールにフォルダが含まれていたか、インストールに何か問題がありましたか?いつの日か、我々はより多くのライブラリがデフォルトで用意されてい拡張配布を提供したいと考えていますが、

+1

ん 'mathcompからのインポートssrnat.'作業が必要? –

+0

これは、 "論理パスにマッチした物理パスが接尾辞<>と接頭辞mathcompに一致するのを見つけることができません" (私にはmathcompがインストールされていません。コックRefmanは 'ssrnat'に言及しているにもかかわらず – LogicChains

+0

が、それが今のように、標準ライブラリにありません(私のインストールは、$ HOME' 'で唯一ssreflect'、' ssrfun'、と 'ssrbool'を持っている/ .opam/4.06.0/lib/coq/plugins/ssr'ディレクトリ)。だから、あなたはmathcompをインストールするべきです。ちなみに、[この質問](https://stackoverflow.com/questions/43955082/how-to-install-ssreflect-and-mathcomp-in-linux)はインストールに役立つかもしれません。 –

答えて

4

ssrnatは、メインのCoqのディストリビューションに含まれていません。

Coq 8.7では、戦術言語自体ssreflectに加えて、いくつかの基本的なサポートライブラリssrfun ssrboolが含まれていました。

ssrnatは数学的な数学的な階層を利用しているので、これはもっと「侵略的な」変化です。

幸いにして、含まれているプラ​​グインのおかげで、ssrnatのインストールは非常に簡単な作業です。

関連する問題