Ecosyste.ms: Issues
An open API service for providing issue and pull request metadata for open source projects.
GitHub / leanprover-community/mathlib4 issues and pull requests
#4197 - feat/refactor: redefinition of homology + derived categories
Pull Request -
State: open - Opened by joelriou over 1 year ago
- 3 comments
Labels: WIP, merge-conflict, new-feature
#2184 - Use `Pairwise` in `Set.iUnionLift` and `Set.liftCover`
Issue -
State: open - Opened by urkud almost 2 years ago
#99 - [Merged by Bors] - feat: add irreducible_def command
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 2 comments
#99 - [Merged by Bors] - feat: add irreducible_def command
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 2 comments
#98 - [Merged by Bors] - chore: bump to nightly-2021-11-17
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 1 comment
#98 - [Merged by Bors] - chore: bump to nightly-2021-11-17
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 1 comment
#97 - [Merged by Bors] - chore: ci: do not install lean 3
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 2 comments
#97 - [Merged by Bors] - chore: ci: do not install lean 3
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 2 comments
#96 - [Merged by Bors] - feat(Tactic): finish implementation of iterate
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
Labels: awaiting-review
#96 - [Merged by Bors] - feat(Tactic): finish implementation of iterate
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
Labels: awaiting-review
#95 - [Merged by Bors] - chore(Tactic/Basic): cleanup and add doc-strings
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 4 comments
Labels: awaiting-review
#95 - [Merged by Bors] - chore(Tactic/Basic): cleanup and add doc-strings
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 4 comments
Labels: awaiting-review
#94 - [Merged by Bors] - fix(Tactic): assumption'
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
Labels: awaiting-review
#94 - [Merged by Bors] - fix(Tactic): assumption'
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
Labels: awaiting-review
#93 - [Merged by Bors] - feat(Tactic/workOnGoal): port workOnGoal from mathlib
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
Labels: awaiting-review
#93 - [Merged by Bors] - feat(Tactic/workOnGoal): port workOnGoal from mathlib
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
Labels: awaiting-review
#92 - add LAKE and LEAN variables to make commands configurable
Pull Request -
State: closed - Opened by stormymcstorm about 3 years ago
- 2 comments
Labels: wontfix
#92 - add LAKE and LEAN variables to make commands configurable
Pull Request -
State: closed - Opened by stormymcstorm about 3 years ago
- 2 comments
Labels: wontfix
#91 - [Merged by Bors] - chore: bump to nightly-2021-11-12
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 2 comments
#91 - [Merged by Bors] - chore: bump to nightly-2021-11-12
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 2 comments
#90 - [Merged by Bors] - feat(Data/UInt, Data/Fin/Basic) declarations
Pull Request -
State: closed - Opened by ammkrn about 3 years ago
- 5 comments
Labels: awaiting-author
#90 - [Merged by Bors] - feat(Data/UInt, Data/Fin/Basic) declarations
Pull Request -
State: closed - Opened by ammkrn about 3 years ago
- 5 comments
Labels: awaiting-author
#89 - [Merged by Bors] - chore: bump to nightly-2021-11-10 and cleanup
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
#89 - [Merged by Bors] - chore: bump to nightly-2021-11-10 and cleanup
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
#88 - feat(Data/UInt, Data/Fin/Basic) instances
Pull Request -
State: closed - Opened by ammkrn about 3 years ago
- 2 comments
#88 - feat(Data/UInt, Data/Fin/Basic) instances
Pull Request -
State: closed - Opened by ammkrn about 3 years ago
- 2 comments
#87 - [Merged by Bors] - fix: add precedence for guardExpr
Pull Request -
State: closed - Opened by dselsam about 3 years ago
- 2 comments
#87 - [Merged by Bors] - fix: add precedence for guardExpr
Pull Request -
State: closed - Opened by dselsam about 3 years ago
- 2 comments
#86 - [Merged by Bors] - chore: bump to lean4:nightly-2021-11-07
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 4 comments
Labels: awaiting-review
#86 - [Merged by Bors] - chore: bump to lean4:nightly-2021-11-07
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 4 comments
Labels: awaiting-review
#85 - [Merged by Bors] - chore: bump to lean4:nightly-2021-11-02
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
#85 - [Merged by Bors] - chore: bump to lean4:nightly-2021-11-02
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
#84 - [Merged by Bors] - feat(Data/Fin/Basic)
Pull Request -
State: closed - Opened by ammkrn about 3 years ago
- 4 comments
#84 - [Merged by Bors] - feat(Data/Fin/Basic)
Pull Request -
State: closed - Opened by ammkrn about 3 years ago
- 4 comments
#83 - [Merged by Bors] - feat(coercion for decidable predicates to bool)
Pull Request -
State: closed - Opened by ammkrn about 3 years ago
- 2 comments
#83 - [Merged by Bors] - feat(coercion for decidable predicates to bool)
Pull Request -
State: closed - Opened by ammkrn about 3 years ago
- 2 comments
#82 - [Merged by Bors] - refactor(remove Decidable.to_bool)
Pull Request -
State: closed - Opened by ammkrn about 3 years ago
- 2 comments
#82 - [Merged by Bors] - refactor(remove Decidable.to_bool)
Pull Request -
State: closed - Opened by ammkrn about 3 years ago
- 2 comments
#81 - [Merged by Bors] - chore: bump to nightly-2021-10-28 and revert regression
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
Labels: awaiting-review
#81 - [Merged by Bors] - chore: bump to nightly-2021-10-28 and revert regression
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
Labels: awaiting-review
#80 - [Merged by Bors] - refactor(Mathport): move mathport prelude to mathlib4
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 4 comments
Labels: awaiting-review
#80 - [Merged by Bors] - refactor(Mathport): move mathport prelude to mathlib4
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 4 comments
Labels: awaiting-review
#79 - [Merged by Bors] - chore(lean-toolchain): bump to nightly-2021-10-26
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
Labels: awaiting-review
#79 - [Merged by Bors] - chore(lean-toolchain): bump to nightly-2021-10-26
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
Labels: awaiting-review
#78 - [Merged by Bors] - refactor(Init): move files which are translations of Lean3 core into Init/
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
Labels: awaiting-review
#78 - [Merged by Bors] - refactor(Init): move files which are translations of Lean3 core into Init/
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
Labels: awaiting-review
#77 - [Merged by Bors] - feat(Init/Data/Nat/Lemmas); nat to string length lemmas
Pull Request -
State: closed - Opened by ammkrn about 3 years ago
- 2 comments
#77 - [Merged by Bors] - feat(Init/Data/Nat/Lemmas); nat to string length lemmas
Pull Request -
State: closed - Opened by ammkrn about 3 years ago
- 2 comments
#76 - [Merged by Bors] - chore: bump to nightly-2021-10-18
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 2 comments
#76 - [Merged by Bors] - chore: bump to nightly-2021-10-18
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 2 comments
#75 - [Merged by Bors] - doc(language): macro guide
Pull Request -
State: closed - Opened by ammkrn about 3 years ago
- 7 comments
#75 - [Merged by Bors] - doc(language): macro guide
Pull Request -
State: closed - Opened by ammkrn about 3 years ago
- 7 comments
#74 - [Merged by Bors] - chore: switch to using lake
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 3 comments
Labels: awaiting-review
#74 - [Merged by Bors] - chore: switch to using lake
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 3 comments
Labels: awaiting-review
#73 - [Merged by Bors] - feat: ext tactic
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 2 comments
#73 - [Merged by Bors] - feat: ext tactic
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 2 comments
#72 - [Merged by Bors] - fix: remove zero diamond
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 2 comments
#72 - [Merged by Bors] - fix: remove zero diamond
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 2 comments
#71 - feat: turn every term into a tactic
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 1 comment
Labels: WIP
#71 - feat: turn every term into a tactic
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 1 comment
Labels: WIP
#70 - [Merged by Bors] - chore: remove split tactic
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 2 comments
#70 - [Merged by Bors] - chore: remove split tactic
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 2 comments
#69 - [Merged by Bors] - fix: `match h 1 with.`
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 4 comments
#69 - [Merged by Bors] - fix: `match h 1 with.`
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 4 comments
#68 - `match h 1 with.` fails with "unexpected discriminant"
Issue -
State: closed - Opened by gebner about 3 years ago
#68 - `match h 1 with.` fails with "unexpected discriminant"
Issue -
State: closed - Opened by gebner about 3 years ago
#67 - [Merged by Bors] - chore: bump to nightly 2021-10-12
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 2 comments
#67 - [Merged by Bors] - chore: bump to nightly 2021-10-12
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 2 comments
#66 - feat(List/String leftpad)
Pull Request -
State: closed - Opened by ammkrn about 3 years ago
#66 - feat(List/String leftpad)
Pull Request -
State: closed - Opened by ammkrn about 3 years ago
#65 - [Merged by Bors] - feat: librarySearch
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 4 comments
#65 - [Merged by Bors] - feat: librarySearch
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 4 comments
#64 - [Merged by Bors] - chore: bump to nightly-2021-10-10
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
#64 - [Merged by Bors] - chore: bump to nightly-2021-10-10
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
#63 - [Merged by Bors] - feat: bump to nightly-2021-10-09
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
#63 - [Merged by Bors] - feat: bump to nightly-2021-10-09
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
#62 - chore(leanpkg.toml): trivial bump to nightly-2021-10-07
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 1 comment
#62 - chore(leanpkg.toml): trivial bump to nightly-2021-10-07
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 1 comment
#61 - [Merged by Bors] - chore: ci: remove leftover from mathlib3
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 1 comment
#61 - [Merged by Bors] - chore: ci: remove leftover from mathlib3
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 1 comment
#60 - [Merged by Bors] - chore: update lean nightly
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 2 comments
#60 - [Merged by Bors] - chore: update lean nightly
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 2 comments
#59 - [Merged by Bors] - feat: List.product
Pull Request -
State: closed - Opened by ammkrn about 3 years ago
- 6 comments
#59 - [Merged by Bors] - feat: List.product
Pull Request -
State: closed - Opened by ammkrn about 3 years ago
- 6 comments
#58 - [Merged by Bors] - chore: remove block tactic
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 2 comments
#58 - [Merged by Bors] - chore: remove block tactic
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 2 comments
#57 - chore: move tests into test directory
Pull Request -
State: closed - Opened by gebner about 3 years ago
#57 - chore: move tests into test directory
Pull Request -
State: closed - Opened by gebner about 3 years ago
#56 - [Merged by Bors] - feat: list permutations and pairwise
Pull Request -
State: closed - Opened by ammkrn about 3 years ago
- 13 comments
#56 - [Merged by Bors] - feat: list permutations and pairwise
Pull Request -
State: closed - Opened by ammkrn about 3 years ago
- 13 comments
#55 - chore(Test/Find): silence tests
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 3 comments
#55 - chore(Test/Find): silence tests
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 3 comments
#54 - [Merged by Bors] - feat(*): bump to nightly-2021-10-02
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
#54 - [Merged by Bors] - feat(*): bump to nightly-2021-10-02
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 2 comments
#53 - [Merged by Bors] - remove Nat.le_of_lt in favor of more general version in Init/Algebra/Order
Pull Request -
State: closed - Opened by dwrensha about 3 years ago
- 2 comments
#53 - [Merged by Bors] - remove Nat.le_of_lt in favor of more general version in Init/Algebra/Order
Pull Request -
State: closed - Opened by dwrensha about 3 years ago
- 2 comments
#52 - [Merged by Bors] - feat: invite bors
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 10 comments
#52 - [Merged by Bors] - feat: invite bors
Pull Request -
State: closed - Opened by gebner about 3 years ago
- 10 comments
#51 - [Merged by Bors] - feat(Tactic/Find): Sebastian's #find command
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 5 comments
#51 - [Merged by Bors] - feat(Tactic/Find): Sebastian's #find command
Pull Request -
State: closed - Opened by semorrison about 3 years ago
- 5 comments