diff src/MoreSpecif.v @ 144:5ea9a0bff8f7

Code for my_tauto
author Adam Chlipala <adamc@hcoop.net>
date Tue, 28 Oct 2008 14:28:22 -0400
parents 6a00d49e85fb
children 54e8ecb5ec88
line wrap: on
line diff
--- a/src/MoreSpecif.v	Tue Oct 28 13:19:33 2008 -0400
+++ b/src/MoreSpecif.v	Tue Oct 28 14:28:22 2008 -0400
@@ -92,3 +92,5 @@
 Delimit Scope partial_scope with partial.
 
 Notation "'Reduce' v" := (if v then Yes else No) : partial_scope.
+Notation "x || y" := (if x then Yes else Reduce y) : partial_scope.
+Notation "x && y" := (if x then Reduce y else No) : partial_scope.