projects
/
coq-hetmet.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
5deda3b
)
General.v: add boolean and/or functions
author
Adam Megacz
<megacz@cs.berkeley.edu>
Fri, 27 May 2011 05:46:43 +0000
(22:46 -0700)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Fri, 27 May 2011 05:46:43 +0000
(22:46 -0700)
src/General.v
patch
|
blob
|
history
diff --git
a/src/General.v
b/src/General.v
index
5d19e9c
..
ae27b9f
100644
(file)
--- a/
src/General.v
+++ b/
src/General.v
@@
-866,6
+866,8
@@
Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))).
(* boolean "not" *)
Definition bnot (b:bool) : bool := if b then false else true.
+Definition band (b1 b2:bool) : bool := if b1 then b2 else false.
+Definition bor (b1 b2:bool) : bool := if b1 then true else b2.
(* string stuff *)
Variable eol : string.