diff options
Diffstat (limited to 'theories/Bool/Sumbool.v')
| -rw-r--r-- | theories/Bool/Sumbool.v | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v index 275712084f..44311a1279 100644 --- a/theories/Bool/Sumbool.v +++ b/theories/Bool/Sumbool.v @@ -8,13 +8,12 @@ (*i $Id$ i*) -(* Here are collected some results about the type sumbool (see INIT/Specif.v) - * [sumbool A B], which is written [{A}+{B}], is the informative - * disjunction "A or B", where A and B are logical propositions. - * Its extraction is isomorphic to the type of booleans. - *) +(** Here are collected some results about the type sumbool (see INIT/Specif.v) + [sumbool A B], which is written [{A}+{B}], is the informative + disjunction "A or B", where A and B are logical propositions. + Its extraction is isomorphic to the type of booleans. *) -(* A boolean is either true or false, and this is decidable *) +(** A boolean is either [true] or [false], and this is decidable *) Lemma sumbool_of_bool : (b:bool) {b=true}+{b=false}. Proof. @@ -36,7 +35,7 @@ Save. (*i pourquoi ce machin-la est dans BOOL et pas dans LOGIC ? Papageno i*) -(* Logic connectives on type sumbool *) +(** Logic connectives on type [sumbool] *) Section connectives. |