Formatting

Author: robin-aws

src/JSON/ConcreteSyntax.SpecProperties.dfy

@@ -4,7 +4,7 @@
 include "ConcreteSyntax.Spec.dfy"
 
 module {:options "-functionSyntax:4"} JSON.ConcreteSyntax.SpecProperties
-// Some useful properties about the functions used in `ConcreteSyntax.Spec`.
+  // Some useful properties about the functions used in `ConcreteSyntax.Spec`.
 {
   import opened BoundedInts
 
@@ -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);

src/JSON/Utils/Seq.dfy

@@ -6,18 +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`
+    // `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`
+    // `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`
+    // `a + b + c + d` is parsed as `((a + b) + c) + d`
     ensures a + b + c + d == a + (b + c + d)
   {}
 }