Mercurial > cpdt > repo

comparison src/Exercises.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 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 *)