erase p in the subst0

agda · Jan 19, 2024 · a838a8c · a838a8c
1 parent cc2a596
commit a838a8c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lib/Haskell/Prelude.agda b/lib/Haskell/Prelude.agda
@@ -125,7 +125,7 @@ lookup x []              = Nothing
 lookup x ((x₁ , y) ∷ xs) = if x == x₁ then Just y else lookup x xs
 
 
-subst0 : (p : @0 a → Set) {@0 x y : a} → @0 x ≡ y → p x → p y
+subst0 : (@0 p : @0 a → Set) {@0 x y : a} → @0 x ≡ y → p x → p y
 subst0 p refl z = z
 {-# COMPILE AGDA2HS subst0 transparent #-}