Merge pull request #524 from mdimjasevic/debruijn-subst-indent

De Bruijn: changes the indentation of function arguments for consistency
2020-10-02 15:34:50 +01:00 · 2020-10-02 15:34:50 +01:00 · 47d08d71fb
commit 47d08d71fb
parent 849807da58 41d7e373ce
1 changed files with 4 additions and 4 deletions
--- a/src/plfa/part2/DeBruijn.lagda.md
+++ b/src/plfa/part2/DeBruijn.lagda.md
@ -692,10 +692,10 @@ variables it is easy to define the special case of
 substitution for one free variable:
 ```
 _[_] : ∀ {Γ A B}
-        → Γ , B ⊢ A
-        → Γ ⊢ B
-          ---------
-        → Γ ⊢ A
+  → Γ , B ⊢ A
+  → Γ ⊢ B
+    ---------
+  → Γ ⊢ A
 _[_] {Γ} {A} {B} N M =  subst {Γ , B} {Γ} σ {A} N
  where
  σ : ∀ {A} → Γ , B ∋ A → Γ ⊢ A