[pre-commit.ci] auto fixes from pre-commit.com hooks

for more information, see https://pre-commit.ci

Author: pre-commit-ci[bot]

src/plfa/part2/DeBruijn.lagda.md

@@ -1058,7 +1058,7 @@ a sequence of length less than the amount of gas and ending in a value.
 data Eval {A} (M : ∅ ⊢ A) (g : ℕ) : Set where
 
   out-of-gas : {N : ∅ ⊢ A}
-    → (M—↠N : M —↠ N)  
+    → (M—↠N : M —↠ N)
     → length M—↠N ≡ g
       ---------------
     → Eval M g
@@ -1395,4 +1395,3 @@ This chapter uses the following unicode:
 --    (done (V-suc (V-suc (V-suc (V-suc V-zero)))))
 -- _ = refl
 -- ```
-

src/plfa/part2/More.lagda.md

@@ -1105,7 +1105,7 @@ length (L —→⟨ L—→M ⟩ M—↠N)  =  suc (length M—↠N)
 data Eval {A} (M : ∅ ⊢ A) (g : ℕ) : Set where
 
   out-of-gas : {N : ∅ ⊢ A}
-    → (M—↠N : M —↠ N)  
+    → (M—↠N : M —↠ N)
     → length M—↠N ≡ g
       ---------------
     → Eval M g

src/plfa/part2/Properties.lagda.md

@@ -878,7 +878,7 @@ well-typed, our evaluator either runs out of gas, returning a sequence
 data Eval (M : Term) (g : ℕ) : Set where
 
   out-of-gas : {N : Term}
-    → (M—↠N : M —↠ N)  
+    → (M—↠N : M —↠ N)
     → length M—↠N ≡ g
       ---------------
     → Eval M g
@@ -938,7 +938,7 @@ remaining.  There are two possibilities:
 
 (Thanks to Conrad Watt for suggesting to relate gas and the length of
 the reduction sequence.)
-      
+
 
 ### Examples
 

src/plfa/part2/Untyped.lagda.md

@@ -557,7 +557,7 @@ normal form.
 data Eval {Γ A} (M : Γ ⊢ A) (g : ℕ) : Set where
 
   out-of-gas : {N : Γ ⊢ A}
-    → (M—↠N : M —↠ N)  
+    → (M—↠N : M —↠ N)
     → length M—↠N ≡ g
       ---------------
     → Eval M g