## Mercurial > cpdt > repo

### comparison src/StackMachine.v @ 534:ed829eaa91b2

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Builds with Coq 8.5beta2

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Wed, 05 Aug 2015 14:46:55 -0400 |

parents | a4b3386ae140 |

children | d65e9c1c9041 |

comparison

equal
deleted
inserted
replaced

533:8921cfa2f503 | 534:ed829eaa91b2 |
---|---|

1 (* Copyright (c) 2008-2012, Adam Chlipala | 1 (* Copyright (c) 2008-2012, 2015, 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: |

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 Set Asymmetric Patterns. | |

19 | 20 |

20 (* begin hide *) | 21 (* begin hide *) |

21 (* begin thide *) | 22 (* begin thide *) |

22 Definition bleh := app_assoc. | 23 Definition bleh := app_assoc. |

23 (* end thide *) | 24 (* end thide *) |

24 (* end hide *) | 25 (* end hide *) |

25 | 26 |

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. *) | 27 (** 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 three 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, and the third allows for more concise pattern-matching syntax in Coq versions 8.5 and higher (having no effect in earlier versions). *) |

27 | 28 |

28 | 29 |

29 (** * Arithmetic Expressions Over Natural Numbers *) | 30 (** * Arithmetic Expressions Over Natural Numbers *) |

30 | 31 |

31 (** We will begin with that staple of compiler textbooks, arithmetic expressions over a single type of numbers. *) | 32 (** We will begin with that staple of compiler textbooks, arithmetic expressions over a single type of numbers. *) |