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 Data.Real.CauSeq #1124

Closed
wants to merge 43 commits into from
Closed

[Merged by Bors] - feat: port Data.Real.CauSeq #1124

Show file tree
Hide file tree
Changes from 34 commits
Commits
Show all changes
43 commits
Select commit Hold shift + click to select a range
85a405e
initial commit
mcdoll Dec 20, 2022
da883b1
fixes
mcdoll Dec 20, 2022
f5cea7f
linter
mcdoll Dec 21, 2022
0c29c34
fixes
mcdoll Dec 21, 2022
1e94c0c
sorried out errors
mcdoll Dec 21, 2022
f806297
merge and fixes
mcdoll Dec 22, 2022
52f6f16
more fixes
mcdoll Dec 22, 2022
cd651a6
coercion hell?
mcdoll Dec 23, 2022
0018c81
Merge branch 'master' of github.com:leanprover-community/mathlib4 int…
mcdoll Dec 24, 2022
f5b2070
one diamond left
mcdoll Dec 24, 2022
527a84a
Merge branch 'master' of github.com:leanprover-community/mathlib4 int…
mcdoll Dec 24, 2022
d4ab366
further narrow down the problem
eric-wieser Dec 24, 2022
d077298
fix
eric-wieser Dec 24, 2022
809e0f6
Merge remote-tracking branch 'origin' into mcdoll/data_real_causeq
mcdoll Dec 26, 2022
f7dd2da
fix build
ChrisHughes24 Dec 26, 2022
c53e87c
comment changes
ChrisHughes24 Dec 26, 2022
1116f94
fix linting errors
ChrisHughes24 Dec 26, 2022
30a934b
line length
ChrisHughes24 Dec 26, 2022
2eadb4a
import in Mathlib.lean
ChrisHughes24 Dec 26, 2022
65ae900
line length
ChrisHughes24 Dec 26, 2022
1d02cb2
Merge remote-tracking branch 'origin/master' into mcdoll/data_real_ca…
eric-wieser Dec 26, 2022
4099908
Merge branch 'master' into mcdoll/data_real_causeq
hrmacbeth Dec 30, 2022
0bf084b
Merge remote-tracking branch 'origin/master' into mcdoll/data_real_ca…
ChrisHughes24 Jan 4, 2023
41bb79d
Apply suggestions from code review
ChrisHughes24 Jan 4, 2023
b24bd0a
lim_zero renaming
ChrisHughes24 Jan 4, 2023
0a717fb
delete commented code
ChrisHughes24 Jan 4, 2023
567c090
add noalign
ChrisHughes24 Jan 4, 2023
6f3b673
restore `norm_cast` attributes
ChrisHughes24 Jan 4, 2023
619a90e
add Porting note:
ChrisHughes24 Jan 4, 2023
3ba5e5f
add latest mathport
eric-wieser Jan 4, 2023
459e2ed
Merge latest mathport into mcdoll/data_real_causeq
eric-wieser Jan 4, 2023
678e846
Merge branch 'mcdoll/data_real_causeq' of github.com:leanprover-commu…
mcdoll Jan 7, 2023
5fb7f2e
Merge remote-tracking branch 'origin' into mcdoll/data_real_causeq
mcdoll Jan 7, 2023
d1134e1
fixes
mcdoll Jan 7, 2023
154f76b
Merge commit 'c2b7c75691a1894b28a403588144aa9ac1a58c08' into HEAD
eric-wieser Jan 7, 2023
b67c547
Merge original mathport into mcdoll/data_real_causeq
eric-wieser Jan 7, 2023
c02aa42
Eric's suggestions
mcdoll Jan 7, 2023
cd317eb
Merge branch 'mcdoll/data_real_causeq' of github.com:leanprover-commu…
mcdoll Jan 7, 2023
6cf1041
fixes
mcdoll Jan 8, 2023
cf9ab7e
Merge remote-tracking branch 'origin/master' into mcdoll/data_real_ca…
Ruben-VandeVelde Jan 9, 2023
bcb7534
Fixes
Ruben-VandeVelde Jan 9, 2023
b381fd1
Better name
Ruben-VandeVelde Jan 9, 2023
46690c3
Reformat
Ruben-VandeVelde Jan 9, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -308,6 +308,7 @@ import Mathlib.Data.Rat.Init
import Mathlib.Data.Rat.Lemmas
import Mathlib.Data.Rat.Order
import Mathlib.Data.Rat.Sqrt
import Mathlib.Data.Real.CauSeq
import Mathlib.Data.Rel
import Mathlib.Data.Semiquot
import Mathlib.Data.Set.Accumulate
Expand Down
Loading