Mercurial > cpdt > repo
comparison src/StackMachine.v @ 513:a4b3386ae140
Get StackMachine template generated properly again
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Thu, 19 Sep 2013 17:28:32 -0400 |
parents | fa2eb72446a8 |
children | ed829eaa91b2 |
comparison
equal
deleted
inserted
replaced
512:6b3fb6672cfa | 513:a4b3386ae140 |
---|---|
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 two lines at the start of the file. *) |
16 | 16 |
17 Require Import Bool Arith List CpdtTactics. | 17 Require Import Bool Arith List CpdtTactics. |
18 Set Implicit Arguments. | 18 Set Implicit Arguments. |
19 | |
20 (* begin hide *) | |
21 (* begin thide *) | |
22 Definition bleh := app_assoc. | |
23 (* end thide *) | |
24 (* end hide *) | |
19 | 25 |
20 (** In general, similar commands will be hidden in the book rendering of each chapter's source code, so you will need to insert them in from-scratch replayings of the code that is presented. To be more specific, every chapter begins with the above two lines, with the import list tweaked as appropriate, considering which definitions the chapter uses. The second command above affects the default behavior of definitions regarding type inference. *) | 26 (** In general, similar commands will be hidden in the book rendering of each chapter's source code, so you will need to insert them in from-scratch replayings of the code that is presented. To be more specific, every chapter begins with the above two lines, with the import list tweaked as appropriate, considering which definitions the chapter uses. The second command above affects the default behavior of definitions regarding type inference. *) |
21 | 27 |
22 | 28 |
23 (** * Arithmetic Expressions Over Natural Numbers *) | 29 (** * Arithmetic Expressions Over Natural Numbers *) |
398 : forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n | 404 : forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n |
399 | 405 |
400 ]] | 406 ]] |
401 | 407 |
402 If we did not already know the name of the theorem, we could use the %\index{Vernacular commands!SearchRewrite}%[SearchRewrite] command to find it, based on a pattern that we would like to rewrite: *) | 408 If we did not already know the name of the theorem, we could use the %\index{Vernacular commands!SearchRewrite}%[SearchRewrite] command to find it, based on a pattern that we would like to rewrite: *) |
403 | |
404 (* begin hide *) | |
405 (* begin thide *) | |
406 Definition bleh := app_assoc. | |
407 (* end thide *) | |
408 (* end hide *) | |
409 | 409 |
410 SearchRewrite ((_ ++ _) ++ _). | 410 SearchRewrite ((_ ++ _) ++ _). |
411 (** %\vspace{-.15in}%[[ | 411 (** %\vspace{-.15in}%[[ |
412 app_assoc_reverse: | 412 app_assoc_reverse: |
413 forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n | 413 forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n |