文件名称：切比
文件大小：113KB
文件格式：ZIP
更新时间：2024-03-09 12:27:43
Coq
切比 该存储库包含有关Chebyshev多项式的一些基本事实的Coq证明。 它是从coqrep库的一个分支开始的，早期版本的历史记录仍可以在相应的存储库中找到。 依赖关系如下：所有文件仅在Coq 8.12上进行测试，并且另外需要mathcomp 1.12。 根据要使用的部分，您将需要其他库：对于在文件“ Cheby_trigo.v”中证明的Chebychev多项式的正交性，您需要Coquelicot 3.1.0，并需要从“ CPoly_I.v”运行间隔算法。 “您将需要Coq-Interval 4.0.0。 一个opam文件提供了显式依赖关系，并允许您编译库 opam pin add -y -n cheby . opam install cheby 文件CPoly_ex.v包含一些我们可以使用此库执行的示例。
【文件预览】：
Cheby-master
----.gitignore(627B)
----generalities.v(27KB)
----opam(668B)
----CPoly_I.v(182KB)
----CPoly_ex.v(12KB)
----Makefile(252B)
----_CoqProject(337B)
----filter_Rlt.v(28KB)
----Rstruct.v(24KB)
----Poly_exec.v(2KB)
----CPoly_interpolation.v(73KB)
----CFun_interpolation.v(35KB)
----arcsinh.v(7KB)
----README.md(830B)
----seq_base.v(4KB)
----CPoly_trigo.v(11KB)
----CPoly.v(26KB)
----Poly_complements.v(2KB)
----CPoly_exec.v(21KB)
----CPoly_iex.v(23KB)
----atan_asin_acos.v(12KB)