refactor: Rising and lowering indices with notation#1348
Conversation
|
Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally. If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks. If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip. Important: If a reviewer adds an |
nateabr
left a comment
nateabr
left a comment
There was a problem hiding this comment.
The changes look great to me, only one minor change would help.
Co-authored-by: nateabr <135662056+nateabr@users.noreply.github.com>
|
Many thanks for reviewing @nateabr! I've incorporated your suggestion. I also made some structural changes to the Elab.lean file to make things hopefully more manifest. Would you mind taking another look? |
nateabr
left a comment
nateabr
left a comment
There was a problem hiding this comment.
This refactor overall is fantastic!
I learned alot about Lean metaprogramming just working this refactor and the new TensorExpressionOperator type.
I had a small question regarding the refactor that I've placed as a comment.
| throwError "Unsupported tensor expression syntax in getIndicesRightEq: {stx}" | ||
|
|
||
| /-! | ||
|
|
There was a problem hiding this comment.
Since the index signature logic is being ported through TensorExpressionOperator, are the index tree scanning functions above still required?
From my understanding this was required with the previous design, so maybe the above could be deleted?
There was a problem hiding this comment.
Awesome! Yep they can be removed - done :).
|
awaiting-author |
github-actions
Bot
added
the
awaiting-author
|
t-relativity |
|
Addressed comment + fixed linters
|
github-actions
Bot
removed
the
awaiting-author
|
-awaiting-author |
nateabr
left a comment
nateabr
left a comment
There was a problem hiding this comment.
Amazing, I humbly submit my first approval to physlib ahahaha.
(I hope this helps you merge)
2 participants
Define
toDualAtIndexwhich rises or lowers a given index of a tensor.Use the elaborator to enable the notation
u | α τ(β)for e.g. rising the second index.Add some test cases, and some explicit examples.