Mercurial > cpdt > repo

comparison src/MoreSpecif.v @ 142:6a00d49e85fb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of Reflection
author Adam Chlipala <adamc@hcoop.net>
date Tue, 28 Oct 2008 11:29:14 -0400
parents 939add5a7db9
children 5ea9a0bff8f7
comparison
equal deleted inserted replaced
141:ce4cc7fa9b2b 142:6a00d49e85fb
71 Notation "e1 ;; e2" := (if e1 then e2 else ??) 71 Notation "e1 ;; e2" := (if e1 then e2 else ??)
72 (right associativity, at level 60) : specif_scope. 72 (right associativity, at level 60) : specif_scope.
73 73
74 Notation "e1 ;;; e2" := (if e1 then e2 else !!) 74 Notation "e1 ;;; e2" := (if e1 then e2 else !!)
75 (right associativity, at level 60) : specif_scope. 75 (right associativity, at level 60) : specif_scope.
76
77
78 Section partial.
79 Variable P : Prop.
80
81 Inductive partial : Set :=
82 | Proved : P -> partial
83 | Uncertain : partial.
84 End partial.
85
86 Notation "[ P ]" := (partial P) : type_scope.
87
88 Notation "'Yes'" := (Proved _) : partial_scope.
89 Notation "'No'" := (Uncertain _) : partial_scope.
90
91 Open Local Scope partial_scope.
92 Delimit Scope partial_scope with partial.
93
94 Notation "'Reduce' v" := (if v then Yes else No) : partial_scope.