From f0ca07c371fd4160f96279f3df99bb24c990b741 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:00:47 +0200
Subject: [PATCH] More: makes A a parameter to the Steps data type (#541)

---
 src/plfa/part2/More.lagda.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/plfa/part2/More.lagda.md b/src/plfa/part2/More.lagda.md
index 2259d5cf..74b5c1d3 100644
--- a/src/plfa/part2/More.lagda.md
+++ b/src/plfa/part2/More.lagda.md
@@ -1105,9 +1105,9 @@ data Finished {Γ A} (N : Γ ⊢ A) : Set where
        ----------
        Finished N
 
-data Steps : ∀ {A} → ∅ ⊢ A → Set where
+data Steps {A} : ∅ ⊢ A → Set where
 
-  steps : ∀ {A} {L N : ∅ ⊢ A}
+  steps : {L N : ∅ ⊢ A}
     → L —↠ N
     → Finished N
       ----------