Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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
[Merged by Bors] - feat: the multiGoal linter #12339
[Merged by Bors] - feat: the multiGoal linter #12339
Changes from all commits
dfe64d6
475c98a
c6e3489
97a7d06
1821772
31d0e2a
fa6d4dd
dc3f312
032028f
f03feb1
214ba12
79fe485
fa9d019
c526603
59042a7
93e1ddf
d912f74
ffc6b69
962c67d
cba8899
080b0c0
75a0e92
ce9a338
1b55583
cfe902d
1b9d82e
1a25287
f16f928
17ba5da
06b9532
3d992a3
c0caa4d
2ecd134
7517f38
77235bb
5f42b76
732c040
ece35d7
4226f06
90aefb0
4de1d51
33d5ee1
b92fc1e
ca0ae70
130941f
05d6947
16d319e
18a70d9
beb1374
16d7500
369da82
11a3ebe
3811f56
7cf0b72
70b9a7f
9327f61
c0c117a
ca1ede0
5e8896b
2943eef
a53f763
44b65ce
f894176
586382b
e13dcbe
cf2f11e
a929633
9fab516
1def34b
bfef0a9
f7a8f88
1f13179
801bd98
4a6adaa
bfa207e
47e3889
a07749b
1240d41
d82b7a7
574aac0
ce49d09
58f7936
2634afb
f4e1bc9
44bf842
b2fd434
068780b
598d773
02fe311
1b34cd8
4df8d9b
eadeffd
31e8639
437e3b2
28a1344
4932699
67a79f8
7717ed0
0883c70
88cb49d
48de0f7
653155a
45a2a7c
78c6e27
37e059f
1ab13f9
18e9f5b
dd46de6
3e9d3e2
File filter
Filter by extension
Conversations
Jump to
There are no files selected for viewing
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thank you; this is much clearer! I'm stumbling a bit over the term "proof branch" - I don't know a better term though. (Do you?)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not really: I view proofs as (syntax) "trees" and this is a "branch" of the "tree"...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Let's get this linter in before the Lean bump :-)