alexjbest
Follow
Highlights
- Pro
Pinned
889 contributions in the last year
Contribution activity
June 2023
Created 18 commits in 5 repositories
Created a pull request in leanprover-community/mathlib4 that received 5 comments
Opened 2 other pull requests in 2 repositories
leanprover/std4
1
merged
leanprover-community/mathlib4
1
closed
Reviewed 6 pull requests in 1 repository
leanprover-community/mathlib4
6 pull requests
- feat: use expected type in set with
- [Merged by Bors] - feat: reimplement the banning of import tactic
- [Merged by Bors] - feat: port Analysis.InnerProductSpace.TwoDim
-
[Merged by Bors] - chore: rename
library_search/propose/rewritestoapply?/have?/rw? -
feat(Tactic/ExtractGoal + test/ExtractGoal): port
extract_goaltactic - [Merged by Bors] - feat: better handling of symm in library_search
Created an issue in leanprover/lean4 that received 1 comment
Declaration silently not added to environment when using local notation
Prerequisites Put an X between the brackets on this line if you have done all of the following: Checked that your issue isn't already filed. Red…
•
1
comment
3
contributions
in private repositories
Jun 13 – Jun 15