New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix examples e.g. u not u_1 in some places, to match VS Code #88

Merged

david-christiansen merged 2 commits into leanprover:master from hmonroe:patch-1

Mar 1, 2024

Contributor

hmonroe commented Dec 15, 2023

No description provided.


          Fix examples e.g. u not u_1 in some places, to match VS Code

18b4c25

Collaborator

david-christiansen commented Mar 1, 2024

At least in today's Lean, #check List shows List.{u} (α : Type u) : Type u, so it's something different again!

I'll update these examples again, then merge.

Thank you!


          fix: Update to current Lean output

d9fdd63

david-christiansen merged commit 2d20c14 into leanprover:master

0 of 2 checks passed

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment