Apply suggestions from code review

Co-authored-by: Mikaël Mayer <[email protected]>
dafny-lang · May 5, 2023 · 35cca47 · 35cca47
1 parent 2753e76
commit 35cca47
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 4 deletions.
diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy
@@ -828,9 +828,8 @@ module {:options "-functionSyntax:4"} Seq {
   }
 
   /* Optimized implementation of Flatten(Map(f, xs)). */
-  function {:opaque} FlatMap<T,R>(f: (T ~> seq<R>), xs: seq<T>): (result: seq<R>)
+  function FlatMap<T,R>(f: (T ~> seq<R>), xs: seq<T>): (result: seq<R>)
     requires forall i :: 0 <= i < |xs| ==> f.requires(xs[i])
-    ensures result == Flatten(Map(f, xs));
     reads set i, o | 0 <= i < |xs| && o in f.reads(xs[i]) :: o
   {
     Flatten(Map(f, xs))

diff --git a/src/JSON/ConcreteSyntax.SpecProperties.dfy b/src/JSON/ConcreteSyntax.SpecProperties.dfy
@@ -21,8 +21,8 @@ module {:options "-functionSyntax:4"} JSON.ConcreteSyntax.SpecProperties
   {
     forall pd0: Suffixed<D, S> --> bytes, pd1: Suffixed<D, S> --> bytes
       | && (forall d | d < bracketed :: pd0.requires(d))
-      && (forall d | d < bracketed :: pd1.requires(d))
-      && (forall d | d < bracketed :: pd0(d) == pd1(d))
+        && (forall d | d < bracketed :: pd1.requires(d))
+        && (forall d | d < bracketed :: pd0(d) == pd1(d))
     {
       calc {
         Spec.Bracketed(bracketed, pd0);

diff --git a/src/JSON/Utils/Seq.dfy b/src/JSON/Utils/Seq.dfy
@@ -6,15 +6,18 @@ module {:options "-functionSyntax:4"} JSON.Utils.Seq {
   {}
 
   lemma Assoc(a: seq, b: seq, c: seq)
+   // `a + b + c` is parsed as `(a + b) + c`
     ensures a + b + c == a + (b + c)
   {}
 
 
   lemma Assoc'(a: seq, b: seq, c: seq)
+   // `a + b + c` is parsed as `(a + b) + c`
     ensures a + (b + c) == a + b + c
   {}
 
   lemma Assoc2(a: seq, b: seq, c: seq, d: seq)
+   // `a + b + c + d` is parsed as `((a + b) + c) + d`
     ensures a + b + c + d == a + (b + c + d)
   {}
 }