Mercurial > cpdt > repo
changeset 201:a2b14ba218a7
Typo reported by mulhern; stop publishing to Harvard
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 02 Jan 2009 09:09:35 -0500 |
parents | df289eb8ef76 |
children | 8caa3b3f8fc0 |
files | Makefile src/InductiveTypes.v |
diffstat | 2 files changed, 2 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/Makefile Fri Jan 02 08:57:25 2009 -0500 +++ b/Makefile Fri Jan 02 09:09:35 2009 -0500 @@ -63,5 +63,5 @@ cp cpdt.tgz staging/ cp latex/cpdt.pdf staging/ cp -R html staging/ - rsync -az --exclude '*~' staging/* bowser.eecs.harvard.edu:public_html/cpdt/book/ +# rsync -az --exclude '*~' staging/* bowser.eecs.harvard.edu:public_html/cpdt/book/ rsync -az --exclude '*~' staging/* ssh.hcoop.net:sites/chlipala/adam/cpdt/
--- a/src/InductiveTypes.v Fri Jan 02 08:57:25 2009 -0500 +++ b/src/InductiveTypes.v Fri Jan 02 09:09:35 2009 -0500 @@ -1137,7 +1137,7 @@ (** %\begin{enumerate}%#<ol># -%\item%#<li># Define an inductive type [truth] with three constructors, [Yes], [No], and [Maybe]. [Yes] stands for certain truth, [False] for certain falsehood, and [Maybe] for an unknown situation. Define "not," "and," and "or" for this replacement boolean algebra. Prove that your implementation of "and" is commutative and distributes over your implementation of "or."#</li># +%\item%#<li># Define an inductive type [truth] with three constructors, [Yes], [No], and [Maybe]. [Yes] stands for certain truth, [No] for certain falsehood, and [Maybe] for an unknown situation. Define "not," "and," and "or" for this replacement boolean algebra. Prove that your implementation of "and" is commutative and distributes over your implementation of "or."#</li># %\item%#<li># Modify the first example language of Chapter 2 to include variables, where variables are represented with [nat]. Extend the syntax and semantics of expressions to accommodate the change. Your new [expDenote] function should take as a new extra first argument a value of type [var -> nat], where [var] is a synonym for naturals-as-variables, and the function assigns a value to each variable. Define a constant folding function which does a bottom-up pass over an expression, at each stage replacing every binary operation on constants with an equivalent constant. Prove that constant folding preserves the meanings of expressions.#</li>#