Skip to content

Commit

Permalink
Update copied check output to corrected universe levels
Browse files Browse the repository at this point in the history
  • Loading branch information
adomasbaliuka authored Aug 29, 2024
1 parent cf2787d commit f14102f
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion lean/main/03_expressions.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
-- []
Expand Down

0 comments on commit f14102f

Please sign in to comment.