[ re #5448 doc ] updated the runtime-irrelevance doc to typecheck.

agda · Sep 30, 2021 · e821bc8 · e821bc8
1 parent 92a5e41
commit e821bc8
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/doc/user-manual/language/runtime-irrelevance.lagda.rst b/doc/user-manual/language/runtime-irrelevance.lagda.rst
@@ -47,7 +47,7 @@ arguments.
 Erasure annotations can also appear in function arguments (both first-order and higher-order). For instance, here is
 an implementation of ``foldl`` on vectors::
 
-  foldl : (B : Nat → Set b)
+  foldl : (B : @0 Nat → Set b)
         → (f : ∀ {@0 n} → B n → A → B (suc n))
         → (z : B 0)
         → ∀ {@0 n} → Vec A n → B n