Mercurial > cpdt > repo
diff src/Subset.v @ 204:cbf2f74a5130
Parts I want to keep compile with 8.2
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 06 Nov 2009 10:52:43 -0500 |
parents | 939add5a7db9 |
children | 3227be370687 |
line wrap: on
line diff
--- a/src/Subset.v Sun Jan 04 08:18:59 2009 -0500 +++ b/src/Subset.v Fri Nov 06 10:52:43 2009 -0500 @@ -376,7 +376,7 @@ We can build "smart" versions of the usual boolean operators and put them to good use in certified programming. For instance, here is a [sumbool] version of boolean "or." *) (* begin thide *) -Notation "x || y" := (if x then Yes else Reduce y) (at level 50). +Notation "x || y" := (if x then Yes else Reduce y). (** Let us use it for building a function that decides list membership. We need to assume the existence of an equality decision procedure for the type of list elements. *)