diff --git a/tests/lean/norm_tac.lean b/tests/lean/norm_tac.lean
index 7f80041e6..fbebfac0c 100644
--- a/tests/lean/norm_tac.lean
+++ b/tests/lean/norm_tac.lean
@@ -1,3 +1,4 @@
+SetOption pp::implicit true
 Variable vector (A : Type) (sz : Nat) : Type
 Variable read {A : Type} {sz : Nat} (v : vector A sz) (i : Nat) (H : i < sz) : A
 Variable V1 : vector Int 10
diff --git a/tests/lean/norm_tac.lean.expected.out b/tests/lean/norm_tac.lean.expected.out
index 1b0754bd0..eabd3fbc4 100644
--- a/tests/lean/norm_tac.lean.expected.out
+++ b/tests/lean/norm_tac.lean.expected.out
@@ -1,5 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
+  Set: lean::pp::implicit
   Assumed: vector
   Assumed: read
   Assumed: V1