Commit 87ca4a52 authored by Quentin Garchery's avatar Quentin Garchery

fix le_mon being lexicographical order

parent c7fbd10a
...@@ -138,7 +138,7 @@ let rec function le_mon (x1 x2: list int) : bool ...@@ -138,7 +138,7 @@ let rec function le_mon (x1 x2: list int) : bool
match x1, x2 with match x1, x2 with
| Nil, _ -> true | Nil, _ -> true
| _, Nil -> false | _, Nil -> false
| Cons v1 r1, Cons v2 r2 -> v1 <= v2 && le_mon r1 r2 | Cons v1 r1, Cons v2 r2 -> v1 < v2 || (v1 = v2 && le_mon r1 r2)
end) end)
let rec function same (l1 l2: list int) : bool let rec function same (l1 l2: list int) : bool
...@@ -388,7 +388,7 @@ let rec function le_mon (x1 x2: list int) : bool ...@@ -388,7 +388,7 @@ let rec function le_mon (x1 x2: list int) : bool
match x1, x2 with match x1, x2 with
| Nil, _ -> true | Nil, _ -> true
| _, Nil -> false | _, Nil -> false
| Cons v1 r1, Cons v2 r2 -> v1 <= v2 && le_mon r1 r2 | Cons v1 r1, Cons v2 r2 -> v1 < v2 || (v1 = v2 && le_mon r1 r2)
end) end)
let rec function same (l1 l2: list int) : bool let rec function same (l1 l2: list int) : bool
......
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