Commit 1af367a5 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Move the Fset.nth function into its own theory, as it causes smt provers to...

Move the Fset.nth function into its own theory, as it causes smt provers to fail on queens.mlw and bellman_ford.mlw.
parent 3a20ca45
......@@ -153,6 +153,13 @@ theory Fset
forall s: set 'a. cardinal s = 1 ->
forall x: 'a. mem x s -> x = choose s
end
theory FsetNth
use import int.Int
use import Fset
function nth (i: int) (s: set 'a) : 'a
axiom nth_injective:
......
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