json: fix bug in qsort algorithm

runtimeverification · Mar 10, 2020 · 1897a94 · 1897a94
1 parent 7cf5277
commit 1897a94
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/json.md b/json.md
@@ -68,11 +68,11 @@ module JSON-EXT
 
     rule #entriesLT(KEY, .JSONs)              => .JSONs
     rule #entriesLT(KEY, (KEY': VALUE, REST)) => KEY': VALUE , #entriesLT(KEY, REST) requires         KEY' <String KEY
-    rule #entriesLT(KEY, (KEY': VALUE, REST)) => KEY': VALUE , #entriesLT(KEY, REST) requires notBool KEY' <String KEY
+    rule #entriesLT(KEY, (KEY': VALUE, REST)) =>               #entriesLT(KEY, REST) requires notBool KEY' <String KEY
 
     rule #entriesGE(KEY, .JSONs)              => .JSONs
     rule #entriesGE(KEY, (KEY': VALUE, REST)) => KEY': VALUE , #entriesGE(KEY, REST) requires         KEY' >=String KEY
-    rule #entriesGE(KEY, (KEY': VALUE, REST)) => KEY': VALUE , #entriesGE(KEY, REST) requires notBool KEY' >=String KEY
+    rule #entriesGE(KEY, (KEY': VALUE, REST)) =>               #entriesGE(KEY, REST) requires notBool KEY' >=String KEY
 
     syntax Bool ::= sortedJSONs ( JSONs ) [function]
  // ------------------------------------------------