Mercurial > cpdt > repo

comparison src/GeneralRec.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 8f9f1e5b2fe3
children 2c8c693ddaba
comparison
equal deleted inserted replaced
533:8921cfa2f503 534:ed829eaa91b2
1 (* Copyright (c) 2006, 2011-2012, Adam Chlipala 1 (* Copyright (c) 2006, 2011-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:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 (* begin hide *) 10 (* begin hide *)
11 Require Import Arith List. 11 Require Import Arith List Omega.
12 12
13 Require Import CpdtTactics Coinductive. 13 Require Import Cpdt.CpdtTactics Cpdt.Coinductive.
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 Set Asymmetric Patterns.
16 (* end hide *) 17 (* end hide *)
17 18
18 19
19 (** %\chapter{General Recursion}% *) 20 (** %\chapter{General Recursion}% *)
20 21