binary_search2: fixed specification

parent 58f2b34e
...@@ -20,8 +20,8 @@ module BinarySearch ...@@ -20,8 +20,8 @@ module BinarySearch
binary_search target lo mid binary_search target lo mid
else else
hi hi
{ f result = target and { f result >= target and
forall x : int. x < result -> f x <> target } forall x : int. x < result -> f x < target }
end end
......
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