leanprover-community / lean4-metaprogramming-book

https://leanprover-community.github.io/lean4-metaprogramming-book/
Apache License 2.0
211 stars 50 forks source link

expressions: add section about universe levels #78

Closed JLimperg closed 1 year ago

JLimperg commented 1 year ago

Depends on #77. Only the last two commits are new.

arthurpaulino commented 1 year ago

There are some conflicts now 🙏🏼

JLimperg commented 1 year ago

Weird that Github wasn't able to figure that out by itself. Should be fixed now. :)