GitHub - ankitku/SoftwareFoundationsExercises: Solving exercises in code downloaded from Software Foundations book by Benjamin C. Pierce et al.

ankitku / SoftwareFoundationsExercises Public

Notifications You must be signed in to change notification settings
Fork 0
Star 0

Solving exercises in code downloaded from Software Foundations book by Benjamin C. Pierce et al.

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 3 Commits
.depend		.depend
.gitignore		.gitignore
Auto.html		Auto.html
Auto.v		Auto.v
Basics.html		Basics.html
Basics.v		Basics.v
Bib.html		Bib.html
Bib.v		Bib.v
Equiv.html		Equiv.html
Equiv.v		Equiv.v
Extraction.html		Extraction.html
Extraction.v		Extraction.v
Hoare.html		Hoare.html
Hoare.v		Hoare.v
Hoare2.html		Hoare2.html
Hoare2.v		Hoare2.v
HoareAsLogic.html		HoareAsLogic.html
HoareAsLogic.v		HoareAsLogic.v
Imp.html		Imp.html
Imp.v		Imp.v
ImpCEvalFun.html		ImpCEvalFun.html
ImpCEvalFun.v		ImpCEvalFun.v
ImpParser.html		ImpParser.html
ImpParser.v		ImpParser.v
IndPrinciples.html		IndPrinciples.html
IndPrinciples.v		IndPrinciples.v
IndProp.html		IndProp.html
IndProp.v		IndProp.v
Induction.html		Induction.html
Induction.v		Induction.v
LICENSE		LICENSE
LibTactics.html		LibTactics.html
LibTactics.v		LibTactics.v
Lists.html		Lists.html
Lists.v		Lists.v
Logic.html		Logic.html
Logic.v		Logic.v
Makefile		Makefile
Maps.html		Maps.html
Maps.v		Maps.v
MoreStlc.html		MoreStlc.html
MoreStlc.v		MoreStlc.v
Norm.html		Norm.html
Norm.v		Norm.v
PE.html		PE.html
PE.v		PE.v
Poly.html		Poly.html
Poly.v		Poly.v
Postscript.html		Postscript.html
Postscript.v		Postscript.v
Preface.html		Preface.html
Preface.v		Preface.v
ProofObjects.html		ProofObjects.html
ProofObjects.v		ProofObjects.v
README		README
RecordSub.html		RecordSub.html
RecordSub.v		RecordSub.v
Records.html		Records.html
Records.v		Records.v
References.html		References.html
References.v		References.v
Rel.html		Rel.html
Rel.v		Rel.v
SfLib.html		SfLib.html
SfLib.v		SfLib.v
Smallstep.html		Smallstep.html
Smallstep.v		Smallstep.v
Stlc.html		Stlc.html
Stlc.v		Stlc.v
StlcProp.html		StlcProp.html
StlcProp.v		StlcProp.v
Sub.html		Sub.html
Sub.v		Sub.v
Symbols.html		Symbols.html
Symbols.v		Symbols.v
Tactics.html		Tactics.html
Tactics.v		Tactics.v
Typechecking.html		Typechecking.html
Typechecking.v		Typechecking.v
Types.html		Types.html
Types.v		Types.v
UseAuto.html		UseAuto.html
UseAuto.v		UseAuto.v
UseTactics.html		UseTactics.html
UseTactics.v		UseTactics.v
coqdoc.css		coqdoc.css
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-bg.jpg		index-bg.jpg
index.html		index.html
jquery-1.8.3.js		jquery-1.8.3.js

Repository files navigation

#########################################################################
                           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