-
Notifications
You must be signed in to change notification settings - Fork 547
Polish lowering chapters and update rules #210
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
Conversation
37193ef
to
e074d40
Compare
e074d40
to
e028ac2
Compare
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.
Nice! Thanks for your continued maintenance of this chapter 😄
I left some comments/suggestions, but overall, LGTM!
I think you missed one:
The given associated type
Projection
is equal toType
; this can be proved
with either normalization or using skolemized types.
(line 120, under ProjectionEq(Projection = Type)
in goals-and-clauses.md)
Also, left a few suggestions using GitHub's new suggestions feature... let me know if that works, so I know whether to keep using it or not.
src/traits/goals-and-clauses.md
Outdated
| Outlives(Type: Region) | ||
| Outlives(Region: Region) | ||
``` | ||
|
||
`WhereClause` refers to a `where` clause that a Rust user would actually be able | ||
to write in a Rust program. This abstraction exists only as a convenience as we | ||
sometimes want to only coope with domain goals that are effectively writable in |
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.
coope?
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.
I wanted to write « cope with » I guess, but now I realize I don’t know if it’s an appropriate verb to use in this context
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.
Perhaps "manipulate"?
Co-Authored-By: scalexm <[email protected]>
Co-Authored-By: scalexm <[email protected]>
Thanks :) |
I updated a bit the lowering-to-logic chapters. In particular, I changed the name of two logical rules: I'll adjust documentation accordingly in rustc and chalk. The implied bounds chapter still needs to be written (which I'm currently doing).