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.
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
[Merged by Bors] - feat: port Control.Fix #1194
Conversation
Mathlib/Control/Fix.lean
Outdated
@@ -67,22 +67,22 @@ it satisfies the equations: | |||
1. `fix f = f (fix f)` (is a fixed point) | |||
2. `∀ X, f X ≤ X → fix f ≤ X` (least fixed point) | |||
-/ | |||
protected def fix (x : α) : Part <| β x := | |||
protected noncomputable def fix (x : α) : Part <| β x := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Add porting notes that noncomputable
was required.
Mathlib/Control/Fix.lean
Outdated
@@ -114,7 +115,7 @@ end Part | |||
|
|||
namespace Part | |||
|
|||
instance : HasFix (Part α) := | |||
noncomputable instance : HasFix (Part α) := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
porting notes on noncomputable
Mathlib/Control/Fix.lean
Outdated
@@ -123,9 +124,8 @@ open Sigma | |||
|
|||
namespace Pi | |||
|
|||
instance Part.hasFix {β} : HasFix (α → Part β) := | |||
noncomputable instance Part.hasFix {β} : HasFix (α → Part β) := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
porting notes on noncomputable
Is there anything further to be done on this PR from my end? |
bors merge |
Mathlib Commit : 207cfac9fcd06138865b5d04f7091e46d9320432 Co-authored-by: Arien Malec <arien.malec@gmail.com> Co-authored-by: Reid Barton <rwbarton@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Mathlib Commit : 207cfac9fcd06138865b5d04f7091e46d9320432