10000 Set relaxedAutoImplicit to false by janmasrovira · Pull Request #7 · anoma/goose-lean · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Set relaxedAutoImplicit to false #7

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
Merged
merged 1 commit into from
Jun 27, 2025
Merged

Set relaxedAutoImplicit to false #7

merged 1 commit into from
Jun 27, 2025

Conversation

janmasrovira
Copy link
Collaborator

I think this is a saner default, and I have already caught one typo with it.

From the documentation:

Automatic implicit parameters insertion is controlled by two options. By default, automatic implicit parameter insertion is relaxed, which means that any unbound identifier may be a candidate for automatic insertion. Setting the option relaxedAutoImplicit to false disables relaxed mode and causes only identifiers that consist of a single character followed by zero or more digits to be considered for automatic insertion.

@janmasrovira janmasrovira self-assigned this Jun 27, 2025
@janmasrovira janmasrovira force-pushed the relaxedAutoImplicit branch from 6760c0a to c9f360a Compare June 27, 2025 15:38
@janmasrovira janmasrovira marked this pull request as ready for review June 27, 2025 15:38
@janmasrovira janmasrovira requested a review from lukaszcz June 27, 2025 15:38
@lukaszcz
Copy link
Collaborator

Yes, I agree, for the kind of stuff we write it's saner.

I guess this default is targeted at math writers, where it becomes really tedious to explicitly list all structures implicit in a definition.

@lukaszcz lukaszcz merged commit 834a3a4 into main Jun 27, 2025
2 checks passed
@lukaszcz lukaszcz deleted the relaxedAutoImplicit branch June 27, 2025 16:04
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@lukaszcz lukaszcz lukaszcz approved these changes

Assignees

@janmasrovira janmasrovira

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@janmasrovira @lukaszcz
0