why3doc index index


(* Axiom of choice *)
module Choice

  use import fn.Fun
  use import option.Option

  constant witness : 'a
  function choice ('a -> bool) : 'a
  axiom choice_def : forall p,x:'a. p x -> p (choice p)

  let ghost choose (p:{'a} -> bool) : {'a}
    requires { exists x. p x }
    ensures { p result }
  = {choice} p

  let ghost choose_if (p:{'a} -> bool) : option {'a}
    returns { None -> forall x. not p x
            | Some u -> p u }
  = let u = {choice} p in if p u then Some u else None

end


Generated by why3doc 0.90+git