Mercurial > cpdt > repo

comparison src/MoreSpecif.v @ 221:54e8ecb5ec88

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Port Reflection
author Adam Chlipala <adamc@hcoop.net>
date Mon, 16 Nov 2009 11:09:47 -0500
parents 5ea9a0bff8f7
children 1f57a8d0ed3d
comparison
equal deleted inserted replaced
220:15501145d696 221:54e8ecb5ec88
15 Notation "!" := (False_rec _ _) : specif_scope. 15 Notation "!" := (False_rec _ _) : specif_scope.
16 Notation "[ e ]" := (exist _ e _) : specif_scope. 16 Notation "[ e ]" := (exist _ e _) : specif_scope.
17 Notation "x <== e1 ; e2" := (let (x, _) := e1 in e2) 17 Notation "x <== e1 ; e2" := (let (x, _) := e1 in e2)
18 (right associativity, at level 60) : specif_scope. 18 (right associativity, at level 60) : specif_scope.
19 19
20 Open Local Scope specif_scope. 20 Local Open Scope specif_scope.
21 Delimit Scope specif_scope with specif. 21 Delimit Scope specif_scope with specif.
22 22
23 Notation "'Yes'" := (left _ _) : specif_scope. 23 Notation "'Yes'" := (left _ _) : specif_scope.
24 Notation "'No'" := (right _ _) : specif_scope. 24 Notation "'No'" := (right _ _) : specif_scope.
25 Notation "'Reduce' x" := (if x then Yes else No) (at level 50) : specif_scope. 25 Notation "'Reduce' x" := (if x then Yes else No) (at level 50) : specif_scope.
86 Notation "[ P ]" := (partial P) : type_scope. 86 Notation "[ P ]" := (partial P) : type_scope.
87 87
88 Notation "'Yes'" := (Proved _) : partial_scope. 88 Notation "'Yes'" := (Proved _) : partial_scope.
89 Notation "'No'" := (Uncertain _) : partial_scope. 89 Notation "'No'" := (Uncertain _) : partial_scope.
90 90
91 Open Local Scope partial_scope. 91 Local Open Scope partial_scope.
92 Delimit Scope partial_scope with partial. 92 Delimit Scope partial_scope with partial.
93 93
94 Notation "'Reduce' v" := (if v then Yes else No) : partial_scope. 94 Notation "'Reduce' v" := (if v then Yes else No) : partial_scope.
95 Notation "x || y" := (if x then Yes else Reduce y) : partial_scope. 95 Notation "x || y" := (if x then Yes else Reduce y) : partial_scope.
96 Notation "x && y" := (if x then Reduce y else No) : partial_scope. 96 Notation "x && y" := (if x then Reduce y else No) : partial_scope.