Commit 9b3951e0 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

new function nth in set.Fset

parent 26729a97
......@@ -134,6 +134,16 @@ theory Fset
forall s: set 'a. cardinal s = 1 ->
forall x: 'a. mem x s -> x = choose s
function nth (i: int) (s: set 'a) : 'a
axiom nth_injective:
forall s: set 'a, i j: int.
0 <= i < cardinal s -> 0 <= j < cardinal s -> nth i s = nth j s -> i = j
axiom nth_surjective:
forall s: set 'a, x: 'a. mem x s ->
exists i: int. 0 <= i < cardinal s -> x = nth i s
end
(* finite sets of integers *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment