Skip to content
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.

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

foo.{$u} is not supported #16

Open
Vtec234 opened this issue Jun 27, 2023 · 0 comments
Open

foo.{$u} is not supported #16

Vtec234 opened this issue Jun 27, 2023 · 0 comments

Comments

@Vtec234
Copy link
Contributor

Vtec234 commented Jun 27, 2023

For consistency, I would expect that when we have u : Level then inside q we could use $u to refer to it. This seems to work sometimes, whereas at other times we need u inside q. The inconsistency is confusing. For example:

open Lean Qq
example (u : Level) (T : Q(Sort u)) (t : Q($T)) := q(@id.{$u} $T $t) -- unknown universe level '«$u»'
example (u : Level) (T : Q(Sort $u)) (t : Q($T)) := q(@id.{$u} $T $t) -- unknown universe level '«$u»'
example (u : Level) (T : Q(Sort u)) (t : Q($T)) := q(@id.{u} $T $t) -- works
example (u : Level) (T : Q(Sort $u)) (t : Q($T)) := q(@id.{u} $T $t) -- works?!
@gebner gebner changed the title Missing name processing for universe levels? foo.{$u} is not supported Jul 16, 2023
eric-wieser added a commit that referenced this issue Aug 18, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant