Mercurial > cpdt > repo

comparison src/StackMachine.v @ 298:123f466faedc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Small tweak to keep things working in 8.2
author Adam Chlipala <adam@chlipala.net>
date Fri, 14 Jan 2011 14:55:32 -0500
parents 1b6c81e51799
children 7b38729be069
comparison
equal deleted inserted replaced
297:b441010125d4 298:123f466faedc
1 (* Copyright (c) 2008-2010, Adam Chlipala 1 (* Copyright (c) 2008-2011, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
19 (** %\chapter{Some Quick Examples}% *) 19 (** %\chapter{Some Quick Examples}% *)
20 20
21 21
22 (** I will start off by jumping right in to a fully-worked set of examples, building certified compilers from increasingly complicated source languages to stack machines. We will meet a few useful tactics and see how they can be used in manual proofs, and we will also see how easily these proofs can be automated instead. This chapter is not meant to give full explanations of the features that are employed. Rather, it is meant more as an advertisement of what is possible. Later chapters will introduce all of the concepts in bottom-up fashion. 22 (** I will start off by jumping right in to a fully-worked set of examples, building certified compilers from increasingly complicated source languages to stack machines. We will meet a few useful tactics and see how they can be used in manual proofs, and we will also see how easily these proofs can be automated instead. This chapter is not meant to give full explanations of the features that are employed. Rather, it is meant more as an advertisement of what is possible. Later chapters will introduce all of the concepts in bottom-up fashion.
23 23
24 I assume that you have installed Coq and Proof General. The code in this book is tested with Coq version 8.2pl2, though parts may work with other versions. 24 I assume that you have installed Coq and Proof General. The code in this book is tested with Coq versions 8.2pl2 and 8.3pl1, though parts may work with other versions.
25 25
26 To set up your Proof General environment to process the source to this chapter, a few simple steps are required. 26 To set up your Proof General environment to process the source to this chapter, a few simple steps are required.
27 27
28 %\begin{enumerate}%#<ol># 28 %\begin{enumerate}%#<ol>#
29 29