mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
7b0929a761
For the previous behaviour (no import), write "use/clone T as T". This shortens the most used "use/clone import" to simply "use/clone".
17 lines
291 B
Plaintext
17 lines
291 B
Plaintext
|
|
module Choice
|
|
|
|
(* no why3 type is empty. *)
|
|
|
|
constant default : 'a
|
|
|
|
(* Axiom of choice : we can explicitely pick an element whom
|
|
existence is proven. *)
|
|
|
|
function choice (p: 'a -> bool) : 'a
|
|
axiom choice_behaviour : forall p: 'a -> bool, x: 'a.
|
|
p x -> p (choice p)
|
|
|
|
end
|
|
|