Skip to content
Snippets Groups Projects
Commit a170be6f authored by Viktor Kuncak's avatar Viktor Kuncak
Browse files

Minor cleanup what is commented and what not.

parent 9d4b0279
No related branches found
No related tags found
No related merge requests found
...@@ -2,18 +2,17 @@ import leon.lang._ ...@@ -2,18 +2,17 @@ import leon.lang._
import leon.lang.synthesis._ import leon.lang.synthesis._
import leon.annotation._ import leon.annotation._
object Max { object Max {
/*
def max(x: Int, y: Int): Int = { def max(x: Int, y: Int): Int = {
val d = x - y val d = x - y
if (d > 0) x if (d > 0) x
else y else y
} ensuring(res => }
x <= res && y <= res && (res == x || res == y)) // ensuring(res => (res == x || res == y))
*/ // x <= res && y <= res
//def test1 = max(10, 5) def test1 = max(10, 5)
//def test2 = max(-5, 5) def test2 = max(-5, 5)
//def test3 = max(-5, -7) def test3 = max(-5, -7)
//def test4 = max(-1639624704, 1879048192) //def test4 = max(-1639624704, 1879048192)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment