切比 源码

切比 该存储库包含有关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