📚 网上馆配 · 在线荐购平台

内容简介：本书包括实数与函数、数列极限、函数极限、函数的连续性、导数和微分、微分中值定理、实数的完备性、不定积分、定积分以及两个特殊极限等内容的形式化实现。在系统中，全部定理无例外地给出Coq的机器证明代码，所有形式化过程已被Coq验证，并在计算机上运行通过，充分体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点。