From f14102fcf6f37e4c1e4a8ea5f025700904dde0cc Mon Sep 17 00:00:00 2001
From: Adomas Baliuka <52975890+adomasbaliuka@users.noreply.github.com>
Date: Thu, 29 Aug 2024 10:48:09 +0200
Subject: [PATCH] Update copied check output to corrected universe levels

---
 lean/main/03_expressions.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean/main/03_expressions.lean b/lean/main/03_expressions.lean
index f63d028..c04b27c 100644
--- a/lean/main/03_expressions.lean
+++ b/lean/main/03_expressions.lean
@@ -301,7 +301,7 @@ elab "mapAddOneNil" : term => return mapAddOneNil
 set_option pp.universes true in
 set_option pp.explicit true in
 #check mapAddOneNil
--- @List.map.{1, 1} Nat Nat (fun x => Nat.add x 1) (@List.nil.{1} Nat) : List.{1} Nat
+-- @List.map.{0, 0} Nat Nat (fun x => x.add 1) (@List.nil.{0} Nat) : List.{0} Nat
 
 #reduce mapAddOneNil
 -- []