Mercurial > cpdt > repo
comparison src/Exercises.v @ 534:ed829eaa91b2
Builds with Coq 8.5beta2
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 05 Aug 2015 14:46:55 -0400 |
parents | 5f25705a10ea |
children |
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: |
8 *) | 8 *) |
9 | 9 |
10 (* begin hide *) | 10 (* begin hide *) |
11 Require Import List. | 11 Require Import List. |
12 | 12 |
13 Require Import CpdtTactics. | 13 Require Import Cpdt.CpdtTactics. |
14 (* end hide *) | 14 (* end hide *) |
15 | 15 |
16 (** These exercises were originally included inline in the text, but my latest feeling is that I don't have the time to maintain the exercises at a sufficient quality level to match the level I'm targetting for the rest of the book. I'm including them in this file for now. *) | 16 (** These exercises were originally included inline in the text, but my latest feeling is that I don't have the time to maintain the exercises at a sufficient quality level to match the level I'm targetting for the rest of the book. I'm including them in this file for now. *) |
17 | 17 |
18 (** * From InductiveTypes *) | 18 (** * From InductiveTypes *) |