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 (*CSC: the URI must disappear: there is a bug now *)
  28 interpretation "boolean not" 'not x = (cic:/matita/datatypes/bool/notb.con x).
  29
  30 definition andb : bool \to bool \to bool\def
  31 \lambda b1,b2:bool.
  32  match b1 with
  33  [ true \Rightarrow
  34         match b2 with [true \Rightarrow true | false \Rightarrow false]
  35  | false \Rightarrow false ].
  36
  37 (*CSC: the URI must disappear: there is a bug now *)
  38 interpretation "boolean and" 'and x y = (cic:/matita/datatypes/bool/andb.con x y).
  39
  40 definition orb : bool \to bool \to bool\def
  41 \lambda b1,b2:bool.
  42  match b1 with
  43  [ true \Rightarrow
  44         match b2 with [true \Rightarrow true | false \Rightarrow false]
  45  | false \Rightarrow false ].
  46
  47 (*CSC: the URI must disappear: there is a bug now *)
  48 interpretation "boolean or" 'or x y = (cic:/matita/datatypes/bool/orb.con x y).
  49
  50 definition if_then_else : bool \to Prop \to Prop \to Prop \def
  51 \lambda b:bool.\lambda P,Q:Prop.
  52 match b with
  53 [ true \Rightarrow P
  54 | false  \Rightarrow Q].
  55
  56 (*CSC: missing notation for if_then_else *)