refactor: improve formatting

Author: ibbem

src/Vatras/Lang/VT.agda

@@ -47,8 +47,7 @@ mutual
   {-|
   Corresponds to ⟦_⟧ on artifacts, options, and choices from the dissertation of Paul Bittner.
   -}
-  configure :
-    ∀ {A} → Configuration → UnrootedVT A → Forest A
+  configure : ∀ {A} → Configuration → UnrootedVT A → Forest A
   configure c (a -< cs >-)        = a -< configure-all c cs >- ∷ []
   configure c (if[ p ]then[ t ])  =
     if (eval p c)

src/Vatras/Translation/Lang/ADT/PropSemantics.agda

@@ -77,7 +77,7 @@ elim-sem P l r c = if eval P c then ⟦ l ⟧ c else ⟦ r ⟧ c
   ≡⟨ if-congˡ (eval P c) (↓-presʳ Q l r c) ⟩
     (if eval P c then ⟦ ↓ Q ⟨ l , r ⟩ ⟧ c else ⟦ r ⟧ c)
   ≡⟨⟩
-    elim-sem P ↓ Q ⟨ l , r ⟩ r c
+    elim-sem P (↓ Q ⟨ l , r ⟩) r c
   ≡⟨ ↓-presʳ P (↓ Q ⟨ l , r ⟩) r c ⟩
     ⟦ ↓ P ⟨ ↓ Q ⟨ l , r ⟩ , r ⟩ ⟧ c
   ∎

src/Vatras/Translation/Lang/VariantList-to-VT.agda

@@ -92,7 +92,7 @@ fnoci-invariant x xs n (suc m) (suc i) c (s≤s i≤m)
 
 module Preservation (A : 𝔸) where
   translate'-preserves-conf : ∀ (x : Forest A) (xs : List (Forest A)) (n : ℕ) (i : ℕ) →
-    configure-all (conf (i + n)) (translate' n x xs ) ≡ VariantList.⟦ x ∷ xs ⟧ i
+    configure-all (conf (i + n)) (translate' n x xs) ≡ VariantList.⟦ x ∷ xs ⟧ i
   translate'-preserves-conf x [] n i =
     begin
       configure-all (conf (i + n)) (encode-forest x)
@@ -187,4 +187,4 @@ VT≽VariantList : VTL ≽ VariantListL
 VT≽VariantList = expressiveness-from-compiler VariantList→VT
 
 VT-is-complete : Complete VTL
-VT-is-complete = completeness-by-expressiveness (VariantList-is-Complete) VT≽VariantList
+VT-is-complete = completeness-by-expressiveness VariantList-is-Complete VT≽VariantList