helm/matita/library/datatypes/bool.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/bool/".
  16
  17 inductive bool : Set \def
  18   | true : bool
  19   | false : bool.
  20
  21 definition notb : bool \to bool \def
  22 \lambda b:bool.
  23  match b with
  24  [ true \Rightarrow false
  25  | false \Rightarrow true ].
  26
  27 definition andb : bool \to bool \to bool\def
  28 \lambda b1,b2:bool.
  29  match b1 with
  30  [ true \Rightarrow
  31         match b2 with [true \Rightarrow true | false \Rightarrow false]
  32  | false \Rightarrow false ].
  33
  34 definition orb : bool \to bool \to bool\def
  35 \lambda b1,b2:bool.
  36  match b1 with
  37  [ true \Rightarrow
  38         match b2 with [true \Rightarrow true | false \Rightarrow false]
  39  | false \Rightarrow false ].
  40
  41 definition if_then_else : bool \to Prop \to Prop \to Prop \def
  42 \lambda b:bool.\lambda P,Q:Prop.
  43 match b with
  44 [ true \Rightarrow P
  45 | false  \Rightarrow Q].