stdlib/bool.mlw

   1
   2 (** {1 Booleans} *)
   3
   4 (** {2 Basic theory of Booleans} *)
   5
   6 module Bool
   7
   8   let function andb (x y : bool) : bool =
   9     match x with
  10     | True -> y
  11     | False -> False
  12     end
  13
  14   let function orb (x y : bool) : bool =
  15     match x with
  16     | False -> y
  17     | True -> True
  18     end
  19
  20   let function notb (x : bool) : bool =
  21     match x with
  22     | False -> True
  23     | True  -> False
  24     end
  25
  26   let function xorb (x y : bool) : bool =
  27     match x with
  28     | False -> y
  29     | True -> notb y
  30     end
  31
  32   let function implb (x y : bool) : bool =
  33     match x with
  34     | False -> True
  35     | True -> y
  36     end
  37
  38   val (=) (x y : bool) : bool ensures { result <-> x = y }
  39
  40 end
  41
  42 (** {2 Operator if-then-else} *)
  43
  44 module Ite
  45
  46   let function ite (b:bool) (x y : 'a) : 'a =
  47     match b with
  48     | True  -> x
  49     | False -> y
  50     end
  51
  52 end