Fixes universe levels in Chapter 03 "Expressions" - Githubissues

leanprover-community / lean4-metaprogramming-book

https://leanprover-community.github.io/lean4-metaprogramming-book/

Apache License 2.0

211 stars 51 forks source link

Fixes universe levels in Chapter 03 "Expressions" #144

Closed adomasbaliuka closed 2 weeks ago

adomasbaliuka commented 1 month ago

Universe level levelOne specified for Nat. Should be levelZero

See zulip discussion

Julian commented 2 weeks ago

Thanks again!