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

Dot-notation helper abbreviations #1346

Closed
leodemoura opened this issue Jul 21, 2022 · 3 comments
Closed

Dot-notation helper abbreviations #1346

leodemoura opened this issue Jul 21, 2022 · 3 comments
Labels
enhancement New feature or request

Comments

@leodemoura
Copy link
Member

During the ICERM after-party hackton, @digama0 suggested we add helper abbreviations such as

abbrev MVarId.getType (mvarId : MVarId) : MetaM Expr

They are great for discoverability when using dot-notation.
@leodemoura leodemoura added the enhancement New feature or request label Jul 21, 2022
leodemoura added a commit that referenced this issue Jul 25, 2022
@leodemoura
refactor: improve MVarId method discoverability
8335a82 
See issue #1346
leodemoura added a commit that referenced this issue Jul 26, 2022
@leodemoura
refactor: improve FVarId method discoverability
90fb110 
See issue #1346
@JLimperg JLimperg mentioned this issue Jul 26, 2022
Closed
@Vtec234 Vtec234 mentioned this issue Jul 27, 2022
Closed
1 task
leodemoura added a commit that referenced this issue Jul 27, 2022
@leodemoura
refactor: add doc strings, cleanup, and dotted notation friendly API
c210781 
See #1346
leodemoura added a commit that referenced this issue Jul 28, 2022
@leodemoura
refactor: improve MVarId method discoverability
6dcba78 
See issue #1346
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this issue Jul 31, 2022
@Vtec234 @digama0
chore: update to nightly-2022-07-28 (#357)
f6714df 
Changed all names related to leanprover/lean4#1346 that I could find.

- [x] leanprover/lean4#1375

Co-authored-by: Wojciech Nawrocki <[email protected]>
Co-authored-by: Mario Carneiro <[email protected]>
@leodemoura
Copy link
Member Author

@digama0 Any other functions to rename?

@digama0
Copy link
Collaborator

digama0 commented Aug 4, 2022

I'm going to be making an in depth pass over everything in the coming weeks, so I'll keep an eye out for dot-notation candidates. But I don't have any suggestions at the moment.

EdAyers pushed a commit to leanprover-community/mathlib4 that referenced this issue Aug 18, 2022
@Vtec234 @digama0 @EdAyers
chore: update to nightly-2022-07-28 (#357)
12cdf0c 
Changed all names related to leanprover/lean4#1346 that I could find.

- [x] leanprover/lean4#1375

Co-authored-by: Wojciech Nawrocki <[email protected]>
Co-authored-by: Mario Carneiro <[email protected]>
@leodemoura
Copy link
Member Author

Closing this issue for now. We can open a new issue for adding new helper abbreviations if someone has suggestions.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement New feature or request
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@digama0 @leodemoura