tests/tests-boolean.mlw

   1
   2 module M
   3
   4   use bool.Bool
   5
   6   let f (a b : bool)
   7     ensures {
   8       (andb (orb a b) (notb (andb a b)) = True)
   9       <->
  10       ( ( a = True \/ b = True ) /\ not ( a = True /\ b = True) )
  11 }
  12   = ()
  13
  14   let g (a b : bool)
  15     ensures {
  16       (xorb a b = True)
  17       <->
  18       ( ( a = True \/ b = True ) /\ not ( a = True /\ b = True) )
  19 }
  20   = ()
  21
  22 end