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.

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

Name clashes between bound variables and symbols: prefer resolving to bound variables #543

Open
ComFreek opened this issue Oct 7, 2020 · 0 comments
Open

Name clashes between bound variables and symbols: prefer resolving to bound variables #543

ComFreek opened this issue Oct 7, 2020 · 0 comments
Assignees
@florian-rabe @Jazzpirate
Labels
bug needs-design parser-lexer Parser, lexer or notation related issues

Comments

@ComFreek
Copy link
Member

ComFreek commented Oct 7, 2020 •
edited
Loading

The following unexpectedly typechecks successfully:

theory TestCase : ur:?LF =
  a : type ❙
  b : type ❙
  x : a ❙
  f : b ⟶ a ❘ = [x: b] x ❙
❚

Problem: This should not typecheck. It typechecks because the token x in the definiens of f is resolved to a reference to the constant x : a and not to the variable bound in [x]. Such weird resolutions (from the user's POV) also happen in right-hand sides of view assignments.

Suggestion: Always prefer resolving tokens to bound variables over resolving them to symbols or notations.
@ComFreek ComFreek added bug needs-design parser-lexer Parser, lexer or notation related issues labels Oct 7, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@florian-rabe florian-rabe

@Jazzpirate Jazzpirate

Labels
bug needs-design parser-lexer Parser, lexer or notation related issues
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@ComFreek @florian-rabe @Jazzpirate