-
Notifications
You must be signed in to change notification settings - Fork 298
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
chore(*): switch to lean 3.6.1 #2064
Merged
Changes from all commits
Commits
Show all changes
57 commits
Select commit
Hold shift + click to select a range
e6f4901
chore(*): switch to lean 3.6.0
gebner 5350fd8
Port `src/linear_algebra` to Lean 3.6c
Vierkantor fc34d93
Port `src/ring_theory` to Lean 3.6c
Vierkantor 158db65
Port `src/algebra` and its dependencies to Lean 3.6c
Vierkantor 1a5d95f
Port `src/group_theory` to Lean 3.6c
Vierkantor 185f76d
WIP: Ports part of `src/data` to Lean 3.6c
Vierkantor 561696f
Port `src/data` (and dependencies) to Lean 3.6
Vierkantor 29aa9ee
fix set_theory.lists
robertylewis 9d66ac2
fix ring2
robertylewis 0e44d29
fix pell.lean
robertylewis 1b5508d
fix dioph.lean
robertylewis 389d5f4
Port `src/number_theory/sum_four_squares.lean` to Lean 3.6c
Vierkantor 4fcd626
Port `src/field_theory` to Lean 3.6
Vierkantor 82bd7bb
Port `src/computability` to Lean 3.6c
Vierkantor 8427582
Port `src/measure_theory` (and dependencies) to Lean 3.6c
Vierkantor a4a51e9
fix manifold/real_instances
robertylewis 767ecc7
fix analysis/complex/polynomial
robertylewis 73f5a7e
Merge remote-tracking branch 'origin/master' into lean36
urkud f8bc1c4
Merge branch 'master' of git://github.com/leanprover-community/mathli…
urkud a9ec482
Fix some compile errors in `real_inner_product`
urkud 15f49bd
Merge remote-tracking branch 'origin/master' into lean36
gebner 9eae01a
Upgrade to Lean 3.6.1
gebner 23c858e
perf: speed up calls to linarith
gebner eebb008
Reduce instance priorities for potentially noncomputable instances.
gebner 0768fc0
Remove cyclic instance.
gebner 88a084f
Make arguments {implicit} in instances where they can be filled in vi…
gebner 38d32c8
Make inner_product_space compile.
gebner 2810d3d
Style.
gebner 5c917ef
Port data.nat.modeq
gebner 0e3081b
Port data.int.parity
gebner e184dd1
Port data.int.modeq
gebner 72cf4e1
Port data.real.hyperreal
gebner d275e43
fix(ci): always run git setup step
robertylewis f809761
Merge remote-tracking branch 'origin/master' into lean36
gebner 778d9d1
Remove pre-3.6 legacy code.
gebner b7d560b
Fix test/monotonicity.lean
gebner 3e282a5
Fix test/ring_exp.lean
gebner b6072a5
Fix test/conv.lean
gebner bceed17
Fix archive/imo1988_q6.lean
gebner 8f9b6c6
Fix docs/tutorial/Zmod37.lean
gebner 9e38477
Fix archive/sensitivity.lean
gebner 83b9a20
refactor(algebra/lie_algebra): lie_algebra should not extend lie_ring
gebner e7823d1
remove unused argument
semorrison b37f486
add doc-string to instance that became a def
semorrison 3beb5f7
add docstring
semorrison b1daf12
Fix linting error ☺
gebner 72af113
Fix data.real.irrational
gebner 23f1ff7
Merge remote-tracking branch 'origin/master' into lean36
gebner 2d4f527
Merge remote-tracking branch 'origin/lie-algebra' into lean36
gebner 748a257
fixing a proof
semorrison 706ecea
cleaning up proof
semorrison 5ad2c87
fix broken proof
semorrison 78dccce
Merge remote-tracking branch 'origin/master' into lean36
semorrison 7bceaee
fix proof
semorrison bad47c3
fix some more proofs
semorrison 9e3332a
fix
semorrison f6649a8
fix proofs
semorrison File filter
Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,7 +1,7 @@ | ||
[package] | ||
name = "mathlib" | ||
version = "0.1" | ||
lean_version = "leanprover-community/lean:3.5.1" | ||
lean_version = "leanprover-community/lean:3.6.1" | ||
path = "src" | ||
|
||
[dependencies] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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.
What's the difference between
inv_inv'
andinv_inv''
? Why do we need both?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.
As far as I can see, the only difference is that
inv_inv'
takesx
as an implicit argument. I think, this should be fixed in the stdlib.