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

RFC: universe could work only on single lines or successive indented lines #2684

Closed
sgouezel opened this issue Oct 14, 2023 · 0 comments · Fixed by #3799
Closed

RFC: universe could work only on single lines or successive indented lines #2684

sgouezel opened this issue Oct 14, 2023 · 0 comments · Fixed by #3799
Labels
RFC Request for comments

Comments

@sgouezel
Copy link

sgouezel commented Oct 14, 2023 •
edited
Loading

Currently,

import Lean

universe u

Open Function Set

works fine. Note that I have misspellt Open instead of open, but this is not a problem since Lean thinks I am declaring a new universe (and in fact three new universes called Open, Function and Set).

To help users not getting trapped by this, it could make sense to have universe only work with a single line, or possibly with several lines but then all of them should be indented. In the latter case, it would be reasonable for symmetry and predictability to require variable to work in the same way, with mandatory indentation on the following lines within the variable declaration.
@sgouezel sgouezel added the RFC Request for comments label Oct 14, 2023
kmill added a commit to kmill/lean4 that referenced this issue Mar 28, 2024
@kmill
fix: require idents come in a column after the start of a command
edb6558 
Commands that can parse an `ident` generally should require that the `ident` use `colGt`. This keeps typos in commands from being interpreted as identifiers.

For example, without this rule,
```
universe u
Open Lean
````
parses the same as `universe u Open Lean`. It would be better to get an error on `Open`.

This PR adds `checkColGt` to `section`, `namespace`, `end`, `variable`, and `universe`.

Closes leanprover#2684
@kmill kmill mentioned this issue Mar 28, 2024
Merged
github-merge-queue bot pushed a commit that referenced this issue Mar 29, 2024
@kmill
fix: require idents come in a column after the start of a command (#…
b15b971 
…3799)

Commands that can optionally parse an `ident` or parse any number of
`ident`s generally should require that the `ident` use `colGt`. This
keeps typos in commands from being interpreted as identifiers.

For example, without this rule,
```
universe u
Open Lean
````
parses the same as `universe u Open Lean`. It would be better to get an
error on `Open`.

This PR adds `checkColGt` to `section`, `namespace`, `end`, `variable`,
and `universe`.

Closes #2684
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
RFC Request for comments
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: require idents come in a column after the start of a command kmill/lean4
1 participant
@sgouezel