projects
/
coq-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
General.v: add boolean and/or functions
[coq-hetmet.git]
/
src
/
General.v
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.
(* 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.
(* string stuff *)
Variable eol : string.