proofs:Coq中的一系列正式证明
需积分: 10 65 浏览量
2021-05-06
10:48:22
上传
评论
收藏 50KB ZIP 举报
proofs-main.zip （63个子文件） 
proofs-main 
.gitignore 164B toast.yml 2KB Makefile 1KB _CoqProject 46B LICENSE.md 1KB .travis.yml 595B .github workflows ci.yml 490B proofs Reflection Reflection.v 2KB README.md 110B Kleene Kleene.v 7KB README.md 178B Intro Lesson4_Extraction.v 1KB Lesson0_Intro.v 1KB README.md 210B Lesson1_DependentTypes.v 1KB Lesson2_Logic.v 4KB Lesson3_Induction.v 2KB Tactics.v 4KB Metatheory Metatheory.v 4KB README.md 227B STLC Semantics.v 1KB Progress.v 676B Preservation.v 2KB Soundness.v 637B Typing.v 1KB README.md 501B FreeVar.v 860B Syntax.v 432B Name.v 697B Substitution.v 593B SystemF Semantics.v 2KB Progress.v 1KB Preservation.v 5KB Soundness.v 686B OpeningSubstitution.v 4KB LocalClosure.v 2KB Typing.v 5KB README.md 682B FreeVar.v 972B Syntax.v 505B Name.v 1KB Substitution.v 7KB Opening.v 8KB Context.v 9KB CategoryTheory Product.v 7KB ProductCategory.v 3KB Coproduct.v 3KB Arrow.v 5KB Category.v 2KB README.md 168B Examples Cat.v 774B Set.v 2KB Maybe.v 4KB Monad.v 1KB NaturalTransformation.v 5KB Terminal.v 1KB Object.v 2KB Initial.v 837B Functor.v 2KB Equivalence.v 2KB scripts lint-general.rb 2KB lint-imports.rb 2KB README.md 708B资源评论
