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