Mercurial > cpdt > repo

comparison src/MoreSpecif.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 3322367e955d
children
comparison
equal deleted inserted replaced
533:8921cfa2f503 534:ed829eaa91b2
1 (* Copyright (c) 2008, 2011, Adam Chlipala 1 (* Copyright (c) 2008, 2011, 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 (* Types and notations presented in Chapter 6 *) 10 (* Types and notations presented in Chapter 6 *)
11 11
12 Set Implicit Arguments. 12 Set Implicit Arguments.
13 Set Asymmetric Patterns.
13 14
14 15
15 Notation "!" := (False_rec _ _) : specif_scope. 16 Notation "!" := (False_rec _ _) : specif_scope.
16 Notation "[ e ]" := (exist _ e _) : specif_scope. 17 Notation "[ e ]" := (exist _ e _) : specif_scope.
17 Notation "x <== e1 ; e2" := (let (x, _) := e1 in e2) 18 Notation "x <== e1 ; e2" := (let (x, _) := e1 in e2)