From 87ca4a52b710d7ad7931f16d497ee5b74dcfdbfd Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 1 Mar 2019 19:24:32 +0100 Subject: [PATCH] fix le_mon being lexicographical order --- examples/in_progress/ring_decision/ringdecision.mlw | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/in_progress/ring_decision/ringdecision.mlw b/examples/in_progress/ring_decision/ringdecision.mlw index 18b7e446d..7150dd3c4 100644 --- a/examples/in_progress/ring_decision/ringdecision.mlw +++ b/examples/in_progress/ring_decision/ringdecision.mlw @@ -138,7 +138,7 @@ let rec function le_mon (x1 x2: list int) : bool match x1, x2 with | Nil, _ -> true | _, 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) let rec function same (l1 l2: list int) : bool @@ -388,7 +388,7 @@ let rec function le_mon (x1 x2: list int) : bool match x1, x2 with | Nil, _ -> true | _, 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) let rec function same (l1 l2: list int) : bool -- GitLab