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: port Logic.Equiv.Option #674

Closed
wants to merge 155 commits into from
Closed

[Merged by Bors] - feat: port Logic.Equiv.Option #674

wants to merge 155 commits into from

Conversation

arienmalec
Copy link
Collaborator

@arienmalec arienmalec commented Nov 22, 2022 •
edited by Ruben-VandeVelde

Initial port for Logic.Equiv.Option -- syntax, naming & many proofs.

Based on 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

semorrison and others added 30 commits November 6, 2022 20:20
@semorrison
port of data.funlike.*
6631370
@semorrison
long line
7700ecf
@semorrison
docBlame
df8ac7f
@semorrison
import
4f074d3
@semorrison
copy and paste mathport output
6170aab
@semorrison
restore lemmas
76bc3e2
@semorrison
Merge branch 'fun_like' into equiv_defs
9bac811
@semorrison
starting
f240c63
@semorrison
rename
246a5c8
@Vierkantor
Fix: Function.Surjective.unique was inferring α : Prop when it ca…
b21f8e8 
…n be any `Sort`
@Vierkantor
Builds until the Quot section
d88f4d8
@Vierkantor
Move to appropriate file
aa3e0d1
@Vierkantor
Revert wrong implicitness
465c82b
@Vierkantor
to_fun_as_coe is useless
487f8b6
@semorrison
merge master
bef5f97
@semorrison
long lines
1239fed
@dwarn
finish last part + capitalisation
95ad701
@semorrison
Merge remote-tracking branch 'origin/master' into equiv_defs
462f3d9
@semorrison
long lines, fix error
5ecbbc1
@semorrison
some additional aligns
bfb9fe4
@semorrison
Merge remote-tracking branch 'origin/master' into equiv_defs
685ac7a
@semorrison
?
889dce5
@pechersky
fix right_inv proof
d5fa3ff
@semorrison
fix again
be11406
@pechersky
Use Logic.Equiv.Defs instead of Data.Equiv.Basic
d6d3b83
@pechersky
fix and speed up Functor map_equiv
8fa0ee6
@semorrison
revert change that hides the simp failure
5f8ae4c
@semorrison
comment out potentially bad simps
97c6582
@semorrison
merge
2b43c57
@Ruben-VandeVelde
Merge branch 'master' into equiv_defs
6c79022
Ruben-VandeVelde
Ruben-VandeVelde requested changes Nov 25, 2022
View reviewed changes
Mathlib/Logic/Equiv/Option.lean Outdated Show resolved Hide resolved
Mathlib/Logic/Equiv/Option.lean Outdated Show resolved Hide resolved
Mathlib/Logic/Equiv/Option.lean Outdated Show resolved Hide resolved
Mathlib/Logic/Equiv/Option.lean Outdated Show resolved Hide resolved
Mathlib/Logic/Equiv/Option.lean Outdated Show resolved Hide resolved
Mathlib/Logic/Equiv/Option.lean Outdated Show resolved Hide resolved
@semorrison
Copy link
Contributor

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Nov 28, 2022
bors bot pushed a commit that referenced this pull request Nov 28, 2022
@semorrison @Vierkantor
@dwarn @pechersky @Ruben-VandeVelde
feat: port Logic.Equiv.Option (#674)
0f9bf8d 
Initial port for Logic.Equiv.Option -- syntax, naming & many proofs.

Based on 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: David Wärn <codwarn@gmail.com>
Co-authored-by: Yakov Pechersky <ypechersky@treeline.bio>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
@semorrison semorrison removed the help-wanted The author needs attention to resolve issues label Nov 28, 2022
@bors
Copy link

bors bot commented Nov 28, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Logic.Equiv.Option [Merged by Bors] - feat: port Logic.Equiv.Option Nov 28, 2022
@bors bors bot closed this Nov 28, 2022
@bors bors bot deleted the port-logic-equiv-option branch November 28, 2022 16:40
rosborn added a commit that referenced this pull request Nov 29, 2022
@rosborn
Merge branch 'master' into Control.Monad.Basic
5b25af6 
* master: (26 commits)
  docs (Order.BoundedOrder): fix typos (#775)
  feat: port Algebra.Order.Monoid.Cancel.Defs (#774)
  feat: port Order.Disjoint (#773)
  feat: port linarith (#526)
  feat: port Algebra.Order.Monoid.Defs (#771)
  feat: port control.functor (#612)
  feat(Algebra/GroupWithZero/Commute): port file (#762)
  feat: port Logic.Equiv.Option (#674)
  chore: fix todos in `to_additive` (#765)
  feat(Algebra/Order/Monoid/MinMax): port file (#763)
  fix: update context in recursive calls in split_ifs (#761)
  feat(Algebra/Regular/Basic): port file (#758)
  feat: port Order.BoundedOrder (#697)
  feat: port Data.Pi.Algebra (#564)
  feat: port Algebra.Hom.Embedding (#764)
  fix: to_additive generates equation lemmas for target (#767)
  fix: fix translation errors in various files (#716)
  fix: remove submodules (#766)
  feat(Algebra/Group/Commute): port file (#750)
  feat(Algebra/Ring/Commute): port file (#759)
  ...
@github-actions github-actions bot mentioned this pull request Nov 29, 2022
Closed
bors bot pushed a commit to leanprover-community/mathlib that referenced this pull request Dec 1, 2022
@leanprover-community-bot
chore(*): add mathlib4 synchronization comments (#17754)
8d89a80 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.field.defs`: leanprover-community/mathlib4#668
* `algebra.group.commute`: leanprover-community/mathlib4#750
* `algebra.group_with_zero.commute`: leanprover-community/mathlib4#762
* `algebra.group_with_zero.semiconj`: leanprover-community/mathlib4#757
* `algebra.group_with_zero.units.basic`: leanprover-community/mathlib4#735
* `algebra.hom.embedding`: leanprover-community/mathlib4#764
* `algebra.order.monoid.cancel.defs`: leanprover-community/mathlib4#774
* `algebra.order.monoid.canonical.defs`: leanprover-community/mathlib4#778
* `algebra.order.monoid.defs`: leanprover-community/mathlib4#771
* `algebra.order.monoid.min_max`: leanprover-community/mathlib4#763
* `algebra.order.monoid.order_dual`: leanprover-community/mathlib4#786
* `algebra.order.sub.defs`: leanprover-community/mathlib4#732
* `algebra.regular.basic`: leanprover-community/mathlib4#758
* `algebra.ring.commute`: leanprover-community/mathlib4#759
* `algebra.ring.regular`: leanprover-community/mathlib4#795
* `algebra.ring.semiconj`: leanprover-community/mathlib4#751
* `control.applicative`: leanprover-community/mathlib4#798
* `control.functor`: leanprover-community/mathlib4#612
* `control.monad.basic`: leanprover-community/mathlib4#752
* `data.countable.defs`: leanprover-community/mathlib4#736
* `data.int.units`: leanprover-community/mathlib4#807
* `data.nat.basic`: leanprover-community/mathlib4#729
* `data.nat.psub`: leanprover-community/mathlib4#806
* `data.nat.units`: leanprover-community/mathlib4#805
* `data.pi.algebra`: leanprover-community/mathlib4#564
* `data.prod.lex`: leanprover-community/mathlib4#783
* `logic.embedding.basic`: leanprover-community/mathlib4#700
* `logic.equiv.option`: leanprover-community/mathlib4#674
* `order.bounded_order`: leanprover-community/mathlib4#697
* `order.with_bot`: leanprover-community/mathlib4#776
* `order.disjoint`: leanprover-community/mathlib4#773
* `order.min_max`: leanprover-community/mathlib4#728
* `order.prop_instances`: leanprover-community/mathlib4#792
* `order.rel_iso.basic`: leanprover-community/mathlib4#772
@github-actions github-actions bot mentioned this pull request Dec 2, 2022
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@semorrison semorrison semorrison left review comments

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde requested changes

Assignees
No one assigned
Labels
mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet