From 2db6d7754fb96e5c157bde3af666799f10c87f43 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= <marko@dimjasevic.net>
Date: Sat, 24 Oct 2020 17:01:09 +0200
Subject: [PATCH] =?UTF-8?q?Make=20=CE=93=20and=20A=20parameters=20instead?=
 =?UTF-8?q?=20of=20indices=20to=20the=20=5F=E2=80=94=E2=86=A0=5F=20relatio?=
 =?UTF-8?q?n=20(#539)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/plfa/part2/DeBruijn.lagda.md | 6 +++---
 src/plfa/part2/More.lagda.md     | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/plfa/part2/DeBruijn.lagda.md b/src/plfa/part2/DeBruijn.lagda.md
index 9b94d5ff..eb07df41 100644
--- a/src/plfa/part2/DeBruijn.lagda.md
+++ b/src/plfa/part2/DeBruijn.lagda.md
@@ -874,13 +874,13 @@ infix  1 begin_
 infixr 2 _—→⟨_⟩_
 infix  3 _∎
 
-data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
+data _—↠_ {Γ A} : (Γ ⊢ A) → (Γ ⊢ A) → Set where
 
-  _∎ : ∀ {Γ A} (M : Γ ⊢ A)
+  _∎ : (M : Γ ⊢ A)
       ------
     → M —↠ M
 
-  _—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
+  _—→⟨_⟩_ : (L : Γ ⊢ A) {M N : Γ ⊢ A}
     → L —→ M
     → M —↠ N
       ------
diff --git a/src/plfa/part2/More.lagda.md b/src/plfa/part2/More.lagda.md
index 74b5c1d3..548ad58a 100644
--- a/src/plfa/part2/More.lagda.md
+++ b/src/plfa/part2/More.lagda.md
@@ -989,13 +989,13 @@ infix  1 begin_
 infixr 2 _—→⟨_⟩_
 infix  3 _∎
 
-data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
+data _—↠_ {Γ A} : (Γ ⊢ A) → (Γ ⊢ A) → Set where
 
-  _∎ : ∀ {Γ A} (M : Γ ⊢ A)
+  _∎ : (M : Γ ⊢ A)
       ------
     → M —↠ M
 
-  _—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
+  _—→⟨_⟩_ : (L : Γ ⊢ A) {M N : Γ ⊢ A}
     → L —→ M
     → M —↠ N
       ------