Skip to content
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 by Bors] - refactor(data/matrix/basic): add matrix.of for type casting #14992

Closed
wants to merge 33 commits into from
Closed

[Merged by Bors] - refactor(data/matrix/basic): add matrix.of for type casting #14992

wants to merge 33 commits into from

Conversation

eric-wieser
Copy link
Member

@eric-wieser eric-wieser commented Jun 27, 2022 •
edited by github-actions bot
Loading

Without this, it is easier to get confused between matrix and pi types, which have different multiplication operators.

With this in place, we can have a special matrix notation that actually produces terms of type matrix.

Open in Gitpod

@eric-wieser
feat(data/matrix/notation): add !ₘ[1, 2; 3, 4] notation
fd80afc
@eric-wieser
add tests, rework
3a2f96e
@eric-wieser
wip
667efdd
@eric-wieser
feat(data/vector/basic): reflected instance for vectors
17702e1 
This means that a `vector` from a tactic block can be used in an expression.
@eric-wieser
no cheating
8d7cc4a
@eric-wieser
Merge remote-tracking branch 'origin/eric-wieser/vector-reflected' in…
a2d169c 
…to eric-wieser/better-matrix-notation
@eric-wieser
Merge remote-tracking branch 'origin/eric-wieser/vector-reflected' in…
e497643 
…to eric-wieser/matrix-wip
@eric-wieser
more wip
194bfee
@eric-wieser
Merge remote-tracking branch 'origin/master' into eric-wieser/better-…
8fa1b0e 
…matrix-notation
@eric-wieser
Merge remote-tracking branch 'origin/master' into eric-wieser/matrix-wip
4a35135
@eric-wieser
working
a33c31c
@eric-wieser
Merge remote-tracking branch 'origin/eric-wieser/better-matrix-notati…
6d13604 
…on' into eric-wieser/matrix-wip
@eric-wieser
lintfix
944f5b4
@eric-wieser
refactor(data/matrix/basic): add matrix.of for type casting
0a93a3e 
Without this, it is easier to get confused between matrix and pi types, which have different multiplication operators.
@eric-wieser eric-wieser added WIP Work in progress awaiting-CI The author would like to see what CI has to say before doing more work. labels Jun 27, 2022
@eric-wieser eric-wieser mentioned this pull request Jun 27, 2022
Closed
@eric-wieser eric-wieser added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jun 29, 2022
@eric-wieser eric-wieser mentioned this pull request Jun 29, 2022
Closed
2 tasks
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jun 30, 2022
@eric-wieser eric-wieser added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Jun 30, 2022
@eric-wieser eric-wieser mentioned this pull request Jul 4, 2022
Closed
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jul 4, 2022
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

Vierkantor
Vierkantor approved these changes Jul 12, 2022
View reviewed changes
Copy link
Collaborator

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks like a good change to me. The main thing is I'm not quite clear on the scope of this change: how did you determine which definitions/lemmas needed the insertion of of? Should everything eventually transition to using of?

src/data/matrix/basic.lean Outdated Show resolved Hide resolved
@eric-wieser
Copy link
Member Author

The main thing is I'm not quite clear on the scope of this change: how did you determine which definitions/lemmas needed the insertion of of

My main approach was to search for lam i j I think, and then fixed everything that broke downstream.
It's not crucial that of is used everywhere, if we miss one then someone will get a nonsense-looking goal they can't make progress on, and we'll find out on Zulip.

I've added a longer module docstring as well as a extension of your suggested comment.

Vierkantor
Vierkantor approved these changes Jul 12, 2022
View reviewed changes
Copy link
Collaborator

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

bors r+

@leanprover-community-bot-assistant leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jul 12, 2022
@Vierkantor
Copy link
Collaborator

Build is failing.

bors r-

bors d+

@bors
Copy link

bors bot commented Jul 12, 2022

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@bors
Copy link

bors bot commented Jul 12, 2022

Canceled.

@github-actions github-actions bot added the delegated The PR author may merge after reviewing final suggestions. label Jul 12, 2022
@eric-wieser
Copy link
Member Author

bors merge

bors bot pushed a commit that referenced this pull request Jul 13, 2022
@eric-wieser
refactor(data/matrix/basic): add matrix.of for type casting (#14992)
6c351a8 
Without this, it is easier to get confused between matrix and pi types, which have different multiplication operators.

With this in place, we can have a special matrix notation that actually produces terms of type `matrix`.
@bors
Copy link

bors bot commented Jul 13, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor(data/matrix/basic): add matrix.of for type casting [Merged by Bors] - refactor(data/matrix/basic): add matrix.of for type casting Jul 13, 2022
@bors bors bot closed this Jul 13, 2022
@bors bors bot deleted the eric-wieser/matrix.of branch July 13, 2022 02:40
joelriou pushed a commit that referenced this pull request Jul 23, 2022
@eric-wieser @joelriou
refactor(data/matrix/basic): add matrix.of for type casting (#14992)
1b43740 
Without this, it is easier to get confused between matrix and pi types, which have different multiplication operators.

With this in place, we can have a special matrix notation that actually produces terms of type `matrix`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Vierkantor Vierkantor Vierkantor approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@eric-wieser @mathlib-dependent-issues-bot @Vierkantor @leanprover-community-bot-assistant