Mercurial > cpdt > repo
comparison src/StackMachine.v @ 536:d65e9c1c9041
Touch-ups in 8.4
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 05 Aug 2015 18:07:57 -0400 |
parents | ed829eaa91b2 |
children | af97676583f3 |
comparison
equal
deleted
inserted
replaced
535:dac7a2705b00 | 536:d65e9c1c9041 |
---|---|
10 | 10 |
11 (** %\chapter{Some Quick Examples}% *) | 11 (** %\chapter{Some Quick Examples}% *) |
12 | 12 |
13 (** 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. In other words, it is expected that most readers will not understand what exactly is going on here, but I hope this demo will whet your appetite for the remaining chapters! | 13 (** 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. In other words, it is expected that most readers will not understand what exactly is going on here, but I hope this demo will whet your appetite for the remaining chapters! |
14 | 14 |
15 As always, you can step through the source file <<StackMachine.v>> for this chapter interactively in Proof General. Alternatively, to get a feel for the whole lifecycle of creating a Coq development, you can enter the pieces of source code in this chapter in a new <<.v>> file in an Emacs buffer. If you do the latter, include these two lines at the start of the file. *) | 15 As always, you can step through the source file <<StackMachine.v>> for this chapter interactively in Proof General. Alternatively, to get a feel for the whole lifecycle of creating a Coq development, you can enter the pieces of source code in this chapter in a new <<.v>> file in an Emacs buffer. If you do the latter, include these three lines at the start of the file. *) |
16 | 16 |
17 Require Import Bool Arith List CpdtTactics. | 17 Require Import Bool Arith List Cpdt.CpdtTactics. |
18 Set Implicit Arguments. | 18 Set Implicit Arguments. |
19 Set Asymmetric Patterns. | 19 Set Asymmetric Patterns. |
20 | 20 |
21 (* begin hide *) | 21 (* begin hide *) |
22 (* begin thide *) | 22 (* begin thide *) |