Skip to content

[Merged by Bors] - feat: port Data.Complex.Exponential#2785

Closed
ChrisHughes24 wants to merge 25 commits intomasterfrom
port/Data.Complex.Exponential
Closed

[Merged by Bors] - feat: port Data.Complex.Exponential#2785
ChrisHughes24 wants to merge 25 commits intomasterfrom
port/Data.Complex.Exponential

Conversation

@ChrisHughes24
Copy link
Copy Markdown
Member

@ChrisHughes24 ChrisHughes24 commented Mar 10, 2023 •
edited
Loading

Lean seems pretty buggy around line 1618. I can't figure out how to get it to even display the right tactic state.

Open in Gitpod

@ChrisHughes24 ChrisHughes24 added help-wanted The author needs attention to resolve issues mathlib-port This is a port of a theory file from mathlib. labels Mar 10, 2023
@ChrisHughes24 ChrisHughes24 added awaiting-review and removed help-wanted The author needs attention to resolve issues labels Mar 13, 2023
@ChrisHughes24
Copy link
Copy Markdown
Member Author

ChrisHughes24 commented Mar 13, 2023

Somebody who understands positivity can fix the extension for exp

@ChrisHughes24 ChrisHughes24 changed the title feat: port/Data.Complex.Exponential feat: port Data.Complex.Exponential Mar 13, 2023
@ChrisHughes24 ChrisHughes24 added WIP Work in progress and removed awaiting-review labels Mar 13, 2023
@ChrisHughes24
Copy link
Copy Markdown
Member Author

ChrisHughes24 commented Mar 13, 2023

@YaelDillies said they could fill in the positivity stuff on Wednesday. There's no huge rush to merge this, so I guess this can wait until Wednesday

@ChrisHughes24 ChrisHughes24 added awaiting-review and removed WIP Work in progress labels Mar 13, 2023
dupuisf
dupuisf reviewed Mar 15, 2023
View reviewed changes
Copy link
Copy Markdown
Contributor

@dupuisf dupuisf 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+

@kim-em kim-em added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Mar 15, 2023
bors bot pushed a commit that referenced this pull request Mar 15, 2023
@ChrisHughes24 @LukasMias
@qawbecrdtey @dwrensha
feat: port Data.Complex.Exponential (#2785)
48b89db 
Co-authored-by: Lukas Miaskiwskyi <lukas.mias@gmail.com>
Co-authored-by: qawbecrdtey <qawbecrdtey@naver.com>
Co-authored-by: David Renshaw <dwrenshaw@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Mar 15, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Data.Complex.Exponential [Merged by Bors] - feat: port Data.Complex.Exponential Mar 15, 2023
@bors bors bot closed this Mar 15, 2023
@bors bors bot deleted the port/Data.Complex.Exponential branch March 15, 2023 17:11
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@dupuisf dupuisf dupuisf left review comments

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.

6 participants

@ChrisHughes24 @dupuisf @kim-em @LukasMias @qawbecrdtey @dwrensha