Mirror of “Software Foundations”, by Benjamin Pierce et al., version 4.0 (May 2016).
Includes a PDF version of the book.
To rebuild the PDF, ensure Coq and LaTeX are installed, then:
$ make
The original Makefile has been modified to work around the LaTeX nesting limit, and to generate chapters in the right order. A syntax error has also been fixed in MoreStlc.v.
diff --git a/src/Makefile b/src/Makefile
index 18ddc1e..9faec71 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -53,7 +53,7 @@ OPT?=
COQDEP?="$(COQBIN)coqdep" -c
COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
COQCHKFLAGS?=-silent -o
-COQDOCFLAGS?=-interpolate -utf8
+COQDOCFLAGS?=-interpolate -utf8 -p '\usepackage{enumitem}\setlistdepth{9}\setlist[itemize,1]{label=$$\bullet$$}\setlist[itemize,2]{label=$$\bullet$$}\setlist[itemize,3]{label=$$\bullet$$}\setlist[itemize,4]{label=$$\bullet$$}\setlist[itemize,5]{label=$$\bullet$$}\setlist[itemize,6]{label=$$\bullet$$}\setlist[itemize,7]{label=$$\bullet$$}\setlist[itemize,8]{label=$$\bullet$$}\setlist[itemize,9]{label=$$\bullet$$}\renewlist{itemize}{itemize}{9}'
COQC?="$(COQBIN)coqc"
GALLINA?="$(COQBIN)gallina"
COQDOC?="$(COQBIN)coqdoc"
@@ -65,7 +65,7 @@ COQCHK?="$(COQBIN)coqchk"
# #
######################
-VFILES:=Symbols.v\
+RVFILES:=Symbols.v\
Preface.v\
Basics.v\
Induction.v\
@@ -106,6 +106,9 @@ VFILES:=Symbols.v\
Postscript.v\
Bib.v
+reverse=$(if $1,$(call reverse,$(wordlist 2,$(words $1),$1))) $(firstword $1)
+VFILES:=$(call reverse,$(RVFILES))
+
-include $(addsuffix .d,$(VFILES))
.SECONDARY: $(addsuffix .d,$(VFILES))
diff --git a/src/MoreStlc.v b/src/MoreStlc.v
index a310fb0..b59a5a1 100644
--- a/src/MoreStlc.v
+++ b/src/MoreStlc.v
@@ -281,7 +281,8 @@ Require Import Stlc.
construct (a very simplified form of Coq's [match]) to destruct
them. For example, the following procedure converts a [Nat+Bool]
into a [Nat]: *)
-(** <<
+(**
+
getNat =
\x:Nat+Bool.
case x ofPackaged by Miëtek Bak.