Why3 Standard Library index



Booleans


Basic theory of Booleans

theory Bool

  use export Bool (* built-in theory of Booleans *)

  function andb (x y : bool) : bool =
    match x with
    | True -> y
    | False -> False
    end

  function orb (x y : bool) : bool =
    match x with
    | False -> y
    | True -> True
    end

  function notb (x : bool) : bool =
    match x with
    | False -> True
    | True  -> False
    end

  function xorb (x y : bool) : bool =
    match x with
    | False -> y
    | True -> notb y
    end

  function implb (x y : bool) : bool =
    match x with
    | False -> True
    | True -> y
    end

end

Operator if-then-else

theory Ite

  use import Bool (* this is the previously declared local theory *)

  function ite (b:bool) (x y : 'a) : 'a =
    match b with
    | True  -> x
    | False -> y
    end

end

Generated by why3doc 0.87.3