GitHub - Smaran-Teja/Logical-Foundations: Coq proof assistant exercises from logical foundations book (from ROCQ Reading Group)

Name		Name	Last commit message	Last commit date
.devcontainer		.devcontainer
.vscode		.vscode
common		common
.AltAuto.aux		.AltAuto.aux
.Auto.aux		.Auto.aux
.Basics.aux		.Basics.aux
.BasicsTest.aux		.BasicsTest.aux
.Bib.aux		.Bib.aux
.DS_Store		.DS_Store
.Extraction.aux		.Extraction.aux
.Imp.aux		.Imp.aux
.ImpCEvalFun.aux		.ImpCEvalFun.aux
.ImpParser.aux		.ImpParser.aux
.IndPrinciples.aux		.IndPrinciples.aux
.IndProp.aux		.IndProp.aux
.Induction.aux		.Induction.aux
.InductionTest.aux		.InductionTest.aux
.Lists.aux		.Lists.aux
.Logic.aux		.Logic.aux
.Makefile.coq.d		.Makefile.coq.d
.Maps.aux		.Maps.aux
.Poly.aux		.Poly.aux
.Postscript.aux		.Postscript.aux
.Preface.aux		.Preface.aux
.PrefaceTest.aux		.PrefaceTest.aux
.ProofObjects.aux		.ProofObjects.aux
.Rel.aux		.Rel.aux
.Tactics.aux		.Tactics.aux
.gitattributes		.gitattributes
.lia.cache		.lia.cache
AltAuto.glob		AltAuto.glob
AltAuto.html		AltAuto.html
AltAuto.v		AltAuto.v
AltAuto.vo		AltAuto.vo
AltAuto.vok		AltAuto.vok
AltAuto.vos		AltAuto.vos
AltAutoTest.v		AltAutoTest.v
Auto.glob		Auto.glob
Auto.html		Auto.html
Auto.v		Auto.v
Auto.vo		Auto.vo
Auto.vok		Auto.vok
Auto.vos		Auto.vos
AutoTest.v		AutoTest.v
Basics.glob		Basics.glob
Basics.html		Basics.html
Basics.v		Basics.v
Basics.vo		Basics.vo
Basics.vok		Basics.vok
Basics.vos		Basics.vos
BasicsTest.glob		BasicsTest.glob
BasicsTest.v		BasicsTest.v
BasicsTest.vo		BasicsTest.vo
BasicsTest.vok		BasicsTest.vok
BasicsTest.vos		BasicsTest.vos
Bib.glob		Bib.glob
Bib.html		Bib.html
Bib.v		Bib.v
Bib.vo		Bib.vo
Bib.vok		Bib.vok
Bib.vos		Bib.vos
BibTest.v		BibTest.v
Extraction.glob		Extraction.glob
Extraction.html		Extraction.html
Extraction.v		Extraction.v
Extraction.vo		Extraction.vo
Extraction.vok		Extraction.vok
Extraction.vos		Extraction.vos
ExtractionTest.v		ExtractionTest.v
Imp.glob		Imp.glob
Imp.html		Imp.html
Imp.v		Imp.v
Imp.vo		Imp.vo
Imp.vok		Imp.vok
Imp.vos		Imp.vos
ImpCEvalFun.glob		ImpCEvalFun.glob
ImpCEvalFun.html		ImpCEvalFun.html
ImpCEvalFun.v		ImpCEvalFun.v
ImpCEvalFun.vo		ImpCEvalFun.vo
ImpCEvalFun.vok		ImpCEvalFun.vok
ImpCEvalFun.vos		ImpCEvalFun.vos
ImpCEvalFunTest.v		ImpCEvalFunTest.v
ImpParser.glob		ImpParser.glob
ImpParser.html		ImpParser.html
ImpParser.v		ImpParser.v
ImpParser.vo		ImpParser.vo
ImpParser.vok		ImpParser.vok
ImpParser.vos		ImpParser.vos
ImpParserTest.v		ImpParserTest.v
ImpTest.v		ImpTest.v
IndPrinciples.glob		IndPrinciples.glob
IndPrinciples.html		IndPrinciples.html
IndPrinciples.v		IndPrinciples.v
IndPrinciples.vo		IndPrinciples.vo
IndPrinciples.vok		IndPrinciples.vok
IndPrinciples.vos		IndPrinciples.vos
IndPrinciplesTest.v		IndPrinciplesTest.v
IndProp.glob		IndProp.glob
IndProp.html		IndProp.html
IndProp.v		IndProp.v

Repository files navigation

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

This directory contains both Coq scripts (.v files) and generated HTML
files for Volume 1 of the Software Foundations electronic textbook
series.

  - 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