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] - feat(data/list): accessing list with fallback #15138

Closed
wants to merge 7 commits into from
Closed

[Merged by Bors] - feat(data/list): accessing list with fallback #15138

wants to merge 7 commits into from

Conversation

pechersky
Copy link
Collaborator

@pechersky pechersky commented Jul 6, 2022 •
edited

Reimplement list.inth in terms of the new list.nthd. Implementation wise, it is "faster" because it doesn't have to go through option.iget on the way anymore.

On the way to computable list-based polynomials

Open in Gitpod

@pechersky
feat(data/list/nthd): accessing list with fallback
bf2ae1d 
Also prove some things about `list.inth` on the way.
On the way to computable list-based polynomials
@pechersky pechersky added the awaiting-review The author would like community review of the PR label Jul 6, 2022
@pechersky pechersky mentioned this pull request Jul 7, 2022
Closed
3 tasks
eric-wieser
eric-wieser reviewed Jul 9, 2022
View reviewed changes
src/data/list/nthd.lean Outdated Show resolved Hide resolved
@pechersky
Define list.inth in terms of list.nthd.
46b6ad8 
Move lemmas into `list/basic`
@pechersky pechersky changed the title feat(data/list/nthd): accessing list with fallback feat(data/list): accessing list with fallback Jul 11, 2022
@pechersky pechersky added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jul 12, 2022
@pechersky pechersky added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 13, 2022
urkud
urkud reviewed Jul 18, 2022
View reviewed changes
src/data/option/basic.lean
@@ -382,6 +382,9 @@ theorem iget_mem [inhabited α] : ∀ {o : option α}, is_some o → o.iget ∈
theorem iget_of_mem [inhabited α] {a : α} : ∀ {o : option α}, a ∈ o → o.iget = a
| _ rfl := rfl

lemma get_or_else_default_eq_iget [inhabited α] (o : option α) : o.get_or_else default = o.iget :=
Copy link
Member

Choose a reason for hiding this comment

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

Idea for the future: redefine option.iget as o.get_or_else default.

@pechersky pechersky requested a review from urkud July 19, 2022 21:03
@urkud
Copy link
Member

urkud commented Jul 20, 2022

Is there a description of the project (computable polynomials) goals and design decisions? Will it be a new type or you're going to redefine polynomial? Will it bring the "non-defeq [decidable_eq]" hell back?

@urkud
Copy link
Member

urkud commented Jul 20, 2022

Anyway, this change LGTM. Thanks!
bors merge

@github-actions github-actions bot 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 20, 2022
bors bot pushed a commit that referenced this pull request Jul 20, 2022
@pechersky
feat(data/list): accessing list with fallback (#15138)
be93cac 
Reimplement `list.inth` in terms of the new `list.nthd`. Implementation wise, it is "faster" because it doesn't have to go through `option.iget` on the way anymore.

On the way to computable list-based polynomials
@pechersky
Copy link
Collaborator Author

pechersky commented Jul 20, 2022 •
edited

Is there a description of the project (computable polynomials) goals and design decisions? Will it be a new type or you're going to redefine polynomial? Will it bring the "non-defeq [decidable_eq]" hell back?

Maybe computable polynomials is a bit overreaching. The goal is #15477. By computable, I mean that one can specify the coefficients explicitly via a "computable" data structure, which can simplify making concrete examples of them.

@bors
Copy link

bors bot commented Jul 20, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/list): accessing list with fallback [Merged by Bors] - feat(data/list): accessing list with fallback Jul 20, 2022
@bors bors bot closed this Jul 20, 2022
@bors bors bot deleted the pechersky/list-nthd branch July 20, 2022 06:04
joelriou pushed a commit that referenced this pull request Jul 23, 2022
@pechersky @joelriou
feat(data/list): accessing list with fallback (#15138)
5e50746 
Reimplement `list.inth` in terms of the new `list.nthd`. Implementation wise, it is "faster" because it doesn't have to go through `option.iget` on the way anymore.

On the way to computable list-based polynomials
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser Awaiting requested review from eric-wieser

@digama0 digama0 Awaiting requested review from digama0

@urkud urkud Awaiting requested review from urkud

Assignees
No one assigned
Labels
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
3 participants
@pechersky @urkud @eric-wieser