GitHub - yunoJ/Coq

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 7 Commits
common		common
.coqdeps.d		.coqdeps.d
Auto.html		Auto.html
Auto.v		Auto.v
AutoTest.v		AutoTest.v
Basics.html		Basics.html
Basics.v		Basics.v
BasicsTest.v		BasicsTest.v
Bib.html		Bib.html
Bib.v		Bib.v
BibTest.v		BibTest.v
Extraction.html		Extraction.html
Extraction.v		Extraction.v
ExtractionTest.v		ExtractionTest.v
Imp.html		Imp.html
Imp.v		Imp.v
ImpCEvalFun.html		ImpCEvalFun.html
ImpCEvalFun.v		ImpCEvalFun.v
ImpCEvalFunTest.v		ImpCEvalFunTest.v
ImpParser.html		ImpParser.html
ImpParser.v		ImpParser.v
ImpParserTest.v		ImpParserTest.v
ImpTest.v		ImpTest.v
IndPrinciples.html		IndPrinciples.html
IndPrinciples.v		IndPrinciples.v
IndPrinciplesTest.v		IndPrinciplesTest.v
IndProp.html		IndProp.html
IndProp.v		IndProp.v
IndPropTest.v		IndPropTest.v
Induction.html		Induction.html
Induction.v		Induction.v
InductionTest.v		InductionTest.v
LICENSE		LICENSE
Lists.html		Lists.html
Lists.v		Lists.v
ListsTest.v		ListsTest.v
Logic.html		Logic.html
Logic.v		Logic.v
LogicTest.v		LogicTest.v
Makefile		Makefile
Maps.html		Maps.html
Maps.v		Maps.v
MapsTest.v		MapsTest.v
Poly.html		Poly.html
Poly.v		Poly.v
PolyTest.v		PolyTest.v
Postscript.html		Postscript.html
Postscript.v		Postscript.v
PostscriptTest.v		PostscriptTest.v
Preface.html		Preface.html
Preface.v		Preface.v
PrefaceTest.v		PrefaceTest.v
ProofObjects.html		ProofObjects.html
ProofObjects.v		ProofObjects.v
ProofObjectsTest.v		ProofObjectsTest.v
README		README
Rel.html		Rel.html
Rel.v		Rel.v
RelTest.v		RelTest.v
Tactics.html		Tactics.html
Tactics.v		Tactics.v
TacticsTest.v		TacticsTest.v
_CoqProject		_CoqProject
coqindex.html		coqindex.html
deps.gif		deps.gif
deps.html		deps.html
deps.map		deps.map
imp.ml		imp.ml
imp.mli		imp.mli
imp1.ml		imp1.ml
imp1.mli		imp1.mli
imp2.ml		imp2.ml
imp2.mli		imp2.mli
impdriver.ml		impdriver.ml
index.html		index.html
toc.html		toc.html

Repository files navigation

<<<<<<< HEAD
#########################################################################
                           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
=======
Learning Coq from Software Foundations.

New .v file will be uploaded whenever I finish a chapter.

Below are discriptions for my coq environment.
-Coq version: 8.9.0
-running on: coqide
-installed with: opam
-machine: ubuntu 18.04
>>>>>>> 12dc326855e9718ad5555b69880ad2b8fb35d394