Coqリストのライブラリが見つかりません

https://coq.inria.fr/distrib/current/stdlib/Coq.Lists.List.htmlのようにconcat関数を使用しようとしています。Coqリストのライブラリが見つかりません

Require Import Arith Coq.Lists.List. 
Import ListNotations. 

Definition CON (l : list nat):= (concat [[0]; l]).

が、私はすでにライブラリをインポートしてきたので、私はこのエラーがどこから来るので、私は知らないが、これは動作するはずと思っエラーError: The reference concat was not found in the current environment.を取得する：私は、次のことを試してみました。

私はバージョン8.4pl3（2014年1月）を使用しています。バージョンの問題かもしれませんか？

出典

2016-05-09 EHM

おそらくはい。私はconcatが追加されたときはわかりませんが、それは8.4pl3後でした – Vinz

はい、それはバージョンの問題です。これは、Coq 8.4pl6のライブラリにはありませんが、Coq 8.5pl1にあります。 –

concatが追加されました。thisコミット。私は8.4pl3のリリースの終わり近くにあったと思うので、リリースにプッシュされたのではなく、むしろ次のリリースにプッシュされたと思う8.5

出典

2016-05-09 11:18:50 Vinz

Coqリストのライブラリが見つかりません

答えて

関連する問題