We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
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
Since 23e7e0b, we can no longer write things like @DHom, because https://github.com/HoTT/HoTT/blob/1a16cbb85d5781325c08881a9c78bae89297101d/theories/Basics/Notations.v#L175
@DHom
Found while rebasing #1302 on master. The workaround is to write @ DHom, but perhaps we want to reconsider the notation.
@ DHom
cc @Alizter , author of 23e7e0b
The text was updated successfully, but these errors were encountered:
Ah that's a shame, we can probably get rid of this notation.
Sorry, something went wrong.
Successfully merging a pull request may close this issue.
Since 23e7e0b, we can no longer write things like
@DHom
, becausehttps://github.com/HoTT/HoTT/blob/1a16cbb85d5781325c08881a9c78bae89297101d/theories/Basics/Notations.v#L175
Found while rebasing #1302 on master. The workaround is to write
@ DHom
, but perhaps we want to reconsider the notation.cc @Alizter , author of 23e7e0b
The text was updated successfully, but these errors were encountered: