Mercurial > cpdt > repo
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.