jiangsy/SoftwareFoundation
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
No description
64 commits 1 branch 0 tags 271 KiB
  • Rocq Prover 95.2%
  • Makefile 4.1%
  • Verilog 0.7%
Find a file
Exact
Shengyi Jiang 45a2de9ab3 finished Imp.v
2019-02-03 21:15:38 +08:00
_CoqProject Tactics.v finished 2019-01-10 17:48:34 +08:00
Auto.v Tactics.v finished 2019-01-10 17:48:34 +08:00
AutoTest.v Tactics.v finished 2019-01-10 17:48:34 +08:00
Basics.v Tactics.v finished 2019-01-10 17:48:34 +08:00
Basics_ex.v Tactics.v finished 2019-01-10 17:48:34 +08:00
BasicsTest.v Tactics.v finished 2019-01-10 17:48:34 +08:00
Bib.v Tactics.v finished 2019-01-10 17:48:34 +08:00
BibTest.v Tactics.v finished 2019-01-10 17:48:34 +08:00
Extraction.v Tactics.v finished 2019-01-10 17:48:34 +08:00
ExtractionTest.v Tactics.v finished 2019-01-10 17:48:34 +08:00
Imp.v finished Imp.v 2019-02-03 21:15:38 +08:00
ImpCEvalFun.v Tactics.v finished 2019-01-10 17:48:34 +08:00
ImpCEvalFunTest.v Tactics.v finished 2019-01-10 17:48:34 +08:00
ImpParser.v Tactics.v finished 2019-01-10 17:48:34 +08:00
ImpParserTest.v Tactics.v finished 2019-01-10 17:48:34 +08:00
ImpTest.v Tactics.v finished 2019-01-10 17:48:34 +08:00
IndPrinciples.v finished IndPrinciples.v 2019-01-29 23:54:28 +08:00
IndPrinciplesTest.v Tactics.v finished 2019-01-10 17:48:34 +08:00
IndProp.v finished lt_trans'' in Rel.v 2019-01-31 23:54:45 +08:00
IndPropTest.v Tactics.v finished 2019-01-10 17:48:34 +08:00
Induction.v Tactics.v finished 2019-01-10 17:48:34 +08:00
Induction_ex.v Tactics.v finished 2019-01-10 17:48:34 +08:00
InductionTest.v Tactics.v finished 2019-01-10 17:48:34 +08:00
LICENSE Tactics.v finished 2019-01-10 17:48:34 +08:00
Lists.v finished Lists.v 2019-01-28 21:18:18 +08:00
ListsTest.v Tactics.v finished 2019-01-10 17:48:34 +08:00
Logic.v finished Logic.v 2019-01-15 00:57:43 +08:00
LogicTest.v Tactics.v finished 2019-01-10 17:48:34 +08:00
Makefile Tactics.v finished 2019-01-10 17:48:34 +08:00
Maps.v finished Maps.v 2019-01-28 19:16:05 +08:00
MapsTest.v Tactics.v finished 2019-01-10 17:48:34 +08:00
Poly.v finishing Poly.v 2019-01-19 21:39:10 +08:00
PolyTest.v Tactics.v finished 2019-01-10 17:48:34 +08:00
Postscript.v Tactics.v finished 2019-01-10 17:48:34 +08:00
PostscriptTest.v Tactics.v finished 2019-01-10 17:48:34 +08:00
Preface.v Tactics.v finished 2019-01-10 17:48:34 +08:00
PrefaceTest.v Tactics.v finished 2019-01-10 17:48:34 +08:00
ProofObjects.v finished ProofObjects.v 2019-01-28 23:53:00 +08:00
ProofObjectsTest.v Tactics.v finished 2019-01-10 17:48:34 +08:00
README Tactics.v finished 2019-01-10 17:48:34 +08:00
Rel.v finished Rel.v 2019-02-01 17:40:16 +08:00
RelTest.v Tactics.v finished 2019-01-10 17:48:34 +08:00
Tactics.v Tactics.v finished 2019-01-10 17:54:54 +08:00
TacticsTest.v Tactics.v finished 2019-01-10 17:48:34 +08:00

README 

#########################################################################
                           SOFTWARE FOUNDATIONS
#########################################################################

This directory contains both Coq scripts (.v files) and more readable
HTML files for the Software Foundations electronic textbook.

  - Preface.v or Preface.html
    The place to start reading, including details on how to install
    required software

  - index.html
    The book's cover page and navigation starting point

  - deps.html 
    Overview of the ordering of chapters

  - LICENSE
    Explanation of how these files may be redistributed