From 00a33e2662210332d059c7e5a38782b3411e8c27 Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@protonmail.com>
Date: Sat, 31 Jul 2021 08:22:49 -0700
Subject: [PATCH] fix: bug in ppExpr test

---
 tests/lean/ppExpr.lean              | 6 +++---
 tests/lean/ppExpr.lean.expected.out | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/tests/lean/ppExpr.lean b/tests/lean/ppExpr.lean
index 642569acef..dcb3a8c19c 100644
--- a/tests/lean/ppExpr.lean
+++ b/tests/lean/ppExpr.lean
@@ -16,11 +16,11 @@ def test (e : Expr) : MetaM Unit := do
 
 -- pp annotations
 #eval test $
-  mkAppN (mkConst `id [levelZero]) #[
+  mkAppN (mkConst `id [levelOne]) #[
     mkConst `Nat,
-    mkMData (KVMap.empty.set `pp.explicit true) $ mkAppN (mkConst `id [levelZero]) #[
+    mkMData (KVMap.empty.set `pp.explicit true) $ mkAppN (mkConst `id [levelOne]) #[
       mkConst `Nat,
-      mkAppN (mkConst `id [levelZero]) #[
+      mkAppN (mkConst `id [levelOne]) #[
         mkConst `Nat,
         mkConst `Nat.zero
   ]]]
diff --git a/tests/lean/ppExpr.lean.expected.out b/tests/lean/ppExpr.lean.expected.out
index 7f766cd51f..cf5d43330f 100644
--- a/tests/lean/ppExpr.lean.expected.out
+++ b/tests/lean/ppExpr.lean.expected.out
@@ -1,3 +1,3 @@
 #0
 fun a => a
-id (α := Nat) ((@id Nat (id (α := Nat) Nat.zero : Nat) : Nat) : Nat)
+id (@id Nat (id Nat.zero))