文件列表:

LICENSE (1079, 2016-09-09)
coq-art/ (0, 2016-09-09)
coq-art/ABriefOverview.v (556, 2016-09-09)
coq-art/DependentProducts.v (7268, 2016-09-09)
coq-art/EverydayLogic.v (19532, 2016-09-09)
coq-art/InductiveDataTypes.v (36834, 2016-09-09)
coq-art/InductivePredicates.v (3770, 2016-09-09)
coq-art/PropostionsAndProofs.v (5547, 2016-09-09)
coq-art/TacticsAndAutomation.v (4799, 2016-09-09)
coq-art/TypesAndExpressions.v (1642, 2016-09-09)
software-foundations/ (0, 2016-09-09)
software-foundations/Basics.v (4870, 2016-09-09)
software-foundations/Imp.v (0, 2016-09-09)
software-foundations/Induction.v (6411, 2016-09-09)
software-foundations/Lists.v (10860, 2016-09-09)
software-foundations/Logic.v (14089, 2016-09-09)
software-foundations/Poly.v (7119, 2016-09-09)
software-foundations/Tactics.v (8551, 2016-09-09)
sqrt-2-irrational/ (0, 2016-09-09)
sqrt-2-irrational/sqrt_2_irrational.v (3245, 2016-09-09)
tsinghua-coq-summer-school/ (0, 2016-09-09)
tsinghua-coq-summer-school/exercises/ (0, 2016-09-09)
tsinghua-coq-summer-school/exercises/exercises_1.v (1022, 2016-09-09)
tsinghua-coq-summer-school/exercises/exercises_2.v (1497, 2016-09-09)
tsinghua-coq-summer-school/exercises/exercises_3.v (4009, 2016-09-09)
tsinghua-coq-summer-school/slides/ (0, 2016-09-09)
tsinghua-coq-summer-school/slides/C1.pdf (192488, 2016-09-09)
tsinghua-coq-summer-school/slides/C2.pdf (104288, 2016-09-09)
tsinghua-coq-summer-school/slides/C3.pdf (1100971, 2016-09-09)
tsinghua-coq-summer-school/solutions/ (0, 2016-09-09)
tsinghua-coq-summer-school/solutions/exercises_1_work.v (4362, 2016-09-09)
tsinghua-coq-summer-school/solutions/exercises_2_work.v (4576, 2016-09-09)
tsinghua-coq-summer-school/solutions/exercises_3_work.v (6070, 2016-09-09)

# amazing-coq WHAT I have done on the road to Coq language and certified programming. Contents -------- + tsinghua-coq-summer-school Code for exercises of _Tsinghua Coq Summer School_ by Yves Bertot and Pierre Castéran. See more details at: [https://www.labri.fr/perso/casteran/CoqArt/Tsinghua/index.html](https://www.labri.fr/perso/casteran/CoqArt/Tsinghua/index.html). + coq-art Code for _Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions_ by Yves Bertot and Pierre Castéran. Coq'Art Home page: [https://www.labri.fr/perso/casteran/CoqArt/](https://www.labri.fr/perso/casteran/CoqArt/). + cpdt Code for _Certified Programming with Dependent Types_ by Adam Chlipala. Book's home page: [http://adam.chlipala.net/cpdt/](http://adam.chlipala.net/cpdt/). + software-foundations Code for _Software Foundations_ by Benjamin C. Pierce. Online version of _Software Foundations_: [https://www.cis.upenn.edu/~bcpierce/sf/current/index.html](https://www.cis.upenn.edu/~bcpierce/sf/current/index.html). License ------- [](https://raw.githubusercontent.com/sighingnow/amazing-coq/master/LICENSE) Open sourced under [The MIT License](LICENSE). Copyright (c) 2015-2016 He Tao.

近期下载者：

相关文件：

评论：[我要评论] [举报此文件]

收藏者：