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
Loading

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

Based on 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

kim-em and others added 30 commits November 6, 2022 20:20
@kim-em
port of data.funlike.*
6631370
@kim-em
long line
7700ecf
@kim-em
docBlame
df8ac7f
@kim-em
import
4f074d3
@kim-em
copy and paste mathport output
6170aab
@kim-em
restore lemmas
76bc3e2
@kim-em
Merge branch 'fun_like' into equiv_defs
9bac811
@kim-em
starting
f240c63
@kim-em
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
@kim-em
merge master
bef5f97
@kim-em
long lines
1239fed
@dwarn
finish last part + capitalisation
95ad701
@kim-em
Merge remote-tracking branch 'origin/master' into equiv_defs
462f3d9
@kim-em
long lines, fix error
5ecbbc1
@kim-em
some additional aligns
bfb9fe4
@kim-em
Merge remote-tracking branch 'origin/master' into equiv_defs
685ac7a
@kim-em
?
889dce5
@pechersky
fix right_inv proof
d5fa3ff
@kim-em
fix again
be11406
@pechersky
Use Logic.Equiv.Defs instead of Data.Equiv.Basic
d6d3b83
@pechersky
fix and speed up Functor map_equiv
8fa0ee6
@kim-em
revert change that hides the simp failure
5f8ae4c
@kim-em
comment out potentially bad simps
97c6582
@kim-em
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
@kim-em
Copy link
Contributor

kim-em commented Nov 28, 2022

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
@kim-em @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 <[email protected]>
Co-authored-by: Anne Baanen <[email protected]>
Co-authored-by: David Wärn <[email protected]>
Co-authored-by: Yakov Pechersky <[email protected]>
Co-authored-by: Ruben Van de Velde <[email protected]>
@kim-em kim-em 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/mathlib3 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

@kim-em kim-em kim-em 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.