[Merged by Bors] - feat: port control.functor by j-loreaux · Pull Request #612 · leanprover-community/mathlib4

j-loreaux · 2022-11-16T07:55:42Z

mathlib3 SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7

depends on: [Merged by Bors] - feat: port Control.Basic #588

Notes:

There is a discrepancy between the Lean 3 and Lean 4 types of has_seq.seq and Seq.seq. I added an ₓ for alignment.
There were one or two places where the existing simp or rw calls didn't succeed, but I'm not entirely sure why.
In Functor.Comp.functor_comp_id and Functor.Comp.functor_id_comp I had to use Id instead of id, because only the former has the Monad instance.
I had to change the imports, but I think what is there now is minimal.

The Kleisli composition operator has binding precedence 55 in Lean 4, and it is a named function, which makes the reason for the existence of `fish` in Lean 3 moot.

bors · 2022-11-28T13:56:16Z

Build failed:

Lint style

…unctor

kim-em · 2022-11-28T14:59:32Z

bors merge

mathlib3 SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7 - [x] depends on: #588 Notes: 1. There is a discrepancy between the Lean 3 and Lean 4 types of `has_seq.seq` and `Seq.seq`. I added an `ₓ` for alignment. 2. There were one or two places where the existing `simp` or `rw` calls didn't succeed, but I'm not entirely sure why. 3. In `Functor.Comp.functor_comp_id` and `Functor.Comp.functor_id_comp` I had to use `Id` instead of `id`, because only the former has the `Monad` instance. 4. I had to change the imports, but I think what is there now is minimal. Co-authored-by: ADedecker <anatolededecker@gmail.com>

bors · 2022-11-28T15:07:16Z

Build failed (retrying...):

Lint style

mathlib3 SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7 - [x] depends on: #588 Notes: 1. There is a discrepancy between the Lean 3 and Lean 4 types of `has_seq.seq` and `Seq.seq`. I added an `ₓ` for alignment. 2. There were one or two places where the existing `simp` or `rw` calls didn't succeed, but I'm not entirely sure why. 3. In `Functor.Comp.functor_comp_id` and `Functor.Comp.functor_id_comp` I had to use `Id` instead of `id`, because only the former has the `Monad` instance. 4. I had to change the imports, but I think what is there now is minimal. Co-authored-by: ADedecker <anatolededecker@gmail.com>

bors · 2022-11-28T15:07:49Z

Build failed (retrying...):

Lint style

mathlib3 SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7 - [x] depends on: #588 Notes: 1. There is a discrepancy between the Lean 3 and Lean 4 types of `has_seq.seq` and `Seq.seq`. I added an `ₓ` for alignment. 2. There were one or two places where the existing `simp` or `rw` calls didn't succeed, but I'm not entirely sure why. 3. In `Functor.Comp.functor_comp_id` and `Functor.Comp.functor_id_comp` I had to use `Id` instead of `id`, because only the former has the `Monad` instance. 4. I had to change the imports, but I think what is there now is minimal. Co-authored-by: ADedecker <anatolededecker@gmail.com>

bors · 2022-11-28T15:08:56Z

Build failed:

Lint style

…unctor

kim-em · 2022-11-28T15:59:23Z

Other PRs have been getting through bors, so I propose we cross our fingers and hope this one will go through when we try again. Once the bors queue is clear, please feel free to try merging again!

bors d+

bors · 2022-11-28T15:59:25Z

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

j-loreaux · 2022-11-28T16:16:23Z

bors r+

mathlib3 SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7 - [x] depends on: #588 Notes: 1. There is a discrepancy between the Lean 3 and Lean 4 types of `has_seq.seq` and `Seq.seq`. I added an `ₓ` for alignment. 2. There were one or two places where the existing `simp` or `rw` calls didn't succeed, but I'm not entirely sure why. 3. In `Functor.Comp.functor_comp_id` and `Functor.Comp.functor_id_comp` I had to use `Id` instead of `id`, because only the former has the `Monad` instance. 4. I had to change the imports, but I think what is there now is minimal. Co-authored-by: ADedecker <anatolededecker@gmail.com>

bors · 2022-11-28T16:17:03Z

Build failed:

Lint style

j-loreaux · 2022-11-28T17:27:42Z

one more try:

bors merge

mathlib3 SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7 - [x] depends on: #588 Notes: 1. There is a discrepancy between the Lean 3 and Lean 4 types of `has_seq.seq` and `Seq.seq`. I added an `ₓ` for alignment. 2. There were one or two places where the existing `simp` or `rw` calls didn't succeed, but I'm not entirely sure why. 3. In `Functor.Comp.functor_comp_id` and `Functor.Comp.functor_id_comp` I had to use `Id` instead of `id`, because only the former has the `Monad` instance. 4. I had to change the imports, but I think what is there now is minimal. Co-authored-by: ADedecker <anatolededecker@gmail.com>

bors · 2022-11-28T17:39:42Z

Pull request successfully merged into master.

Build succeeded:

bors · 2022-11-28T17:39:47Z

Pull request successfully merged into master.

Build succeeded:

* 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) ...

ADedecker and others added 11 commits November 12, 2022 22:34

Begin

ed6930b

Problem with mapConstRev

545f22f

Most done

b1227a3

Follow naming conventions for monads

01bdbd0

Add warnings back, rename

e3813a9

Fix

41b1635

Merge branch 'AD_PORT_control_basic' into j-loreaux/control.functor

9609cc6

raw mathport

07a35ef

get it compiling

22fe7a0

update names and docstrings

a8ae6df

fix module docstring

83d1d38

j-loreaux added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) awaiting-review mathlib-port This is a port of a theory file from mathlib. labels Nov 16, 2022

j-loreaux added 16 commits November 17, 2022 09:15

fix module docstring

331221b

remove unnecessary section and comment out notation

551bc46

docstrings

3409637

#align with ₓ for dubious translations

582a4f5

try to appease check_univs linter

12e8755

remove notation $<

cbe7c6c

remove dubious translation warnings

8fa98e8

remove fish definition entirely

3974e7e

The Kleisli composition operator has binding precedence 55 in Lean 4, and it is a named function, which makes the reason for the existence of `fish` in Lean 3 moot.

fix fish_assoc

8ece2e0

fix > 100 chars

a89877c

add module docstring

ee5dc23

fix indentation

87a1f01

appease checkUnivs linter

d242aaf

oops, remove lint imports

863c568

fix import order

330726a

Merge branch 'AD_PORT_control_basic' into j-loreaux/control.functor

82b5f65

Merge remote-tracking branch 'origin/master' into j-loreaux/control.f…

3523448

…unctor

Merge remote-tracking branch 'origin/master' into j-loreaux/control.f…

7cfa949

…unctor

kim-em added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed ready-to-merge This PR has been sent to bors. labels Nov 28, 2022

j-loreaux mentioned this pull request Nov 28, 2022

feat(Control/Functor): port file #769

Closed

1 task

Merge branch 'master' into j-loreaux/control.functor

669ad19

bors bot changed the title ~~feat: port control.functor~~ [Merged by Bors] - feat: port control.functor Nov 28, 2022

bors bot closed this Nov 28, 2022

bors bot deleted the j-loreaux/control.functor branch November 28, 2022 17:39

github-actions bot mentioned this pull request Nov 29, 2022

[Merged by Bors] - chore(*): add mathlib4 synchronization comments leanprover-community/mathlib3#17754

Closed

github-actions bot mentioned this pull request Dec 2, 2022

[Merged by Bors] - chore(*): add mathlib4 synchronization comments leanprover-community/mathlib3#17790

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: port control.functor#612

[Merged by Bors] - feat: port control.functor#612
j-loreaux wants to merge 39 commits intomasterfrom
j-loreaux/control.functor

j-loreaux commented Nov 16, 2022 •

edited

Loading

Uh oh!

bors bot commented Nov 28, 2022

Uh oh!

kim-em commented Nov 28, 2022

Uh oh!

bors bot commented Nov 28, 2022

Uh oh!

bors bot commented Nov 28, 2022

Uh oh!

bors bot commented Nov 28, 2022

Uh oh!

kim-em commented Nov 28, 2022

Uh oh!

bors bot commented Nov 28, 2022

Uh oh!

j-loreaux commented Nov 28, 2022

Uh oh!

bors bot commented Nov 28, 2022

Uh oh!

j-loreaux commented Nov 28, 2022

Uh oh!

bors bot commented Nov 28, 2022

Uh oh!

bors bot commented Nov 28, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

j-loreaux commented Nov 16, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

bors bot commented Nov 28, 2022

Uh oh!

kim-em commented Nov 28, 2022

Uh oh!

bors bot commented Nov 28, 2022

Uh oh!

bors bot commented Nov 28, 2022

Uh oh!

bors bot commented Nov 28, 2022

Uh oh!

kim-em commented Nov 28, 2022

Uh oh!

bors bot commented Nov 28, 2022

Uh oh!

j-loreaux commented Nov 28, 2022

Uh oh!

bors bot commented Nov 28, 2022

Uh oh!

j-loreaux commented Nov 28, 2022

Uh oh!

bors bot commented Nov 28, 2022

Uh oh!

bors bot commented Nov 28, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

j-loreaux commented Nov 16, 2022 •

edited

Loading