Skip to content
This repository was archived by the owner on Aug 5, 2024. It is now read-only.

Pull requests: leanprover/lean3-mode

Clear current search query, filters, and sorts
0 Open 25 Closed
0 Open 25 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Fix #45.
#46 by jmbr was merged Jun 11, 2023 Loading…
Lean the mode
#44 by sirikid was closed Mar 15, 2023 Loading…
1
Add weakly covers symbol and opposites shortcuts
#41 by YaelDillies was merged May 1, 2022 Loading…
Add covers symbol and blackboard letters
#40 by YaelDillies was merged Jan 24, 2022 Loading…
Add \specializes → ⤳ abbreviation
#39 by erdOne was merged Dec 20, 2021 Loading…
Abbreviations \/ and \quot for ⧸
#38 by Vierkantor was merged Dec 3, 2021 Loading…
Add some quality of life changes
#37 by Zetagon was merged May 2, 2021 Loading…
3
feat(*): port to eldoc handling of emacs 28
#34 by kritixilithos was merged Apr 6, 2021 Loading…
1
Replace deprecated dash-functional dependency
#32 by basil-conto was merged Mar 5, 2021 Loading…
chore: require lean-info in lean-type
#31 by collares was merged Feb 9, 2021 Loading…
Make sure each file byte-compiles by itself with no errors
#30 by collares was merged Sep 30, 2020 Loading…
1
Change functor arrow to rightwards harpoon
#29 by kmill was merged Feb 9, 2021 Loading…
Clarifying the readme, and a typo
#28 by kmill was merged Jun 20, 2020 Loading…
Reuse the window for info buffers
#27 by kmill was merged Jun 20, 2020 Loading…
1
Change the requires-pattern in helm-lean
#26 by kmill was merged Jun 20, 2020 Loading…
Modified overlays for the message boxes
#25 by kmill was merged Jun 20, 2020 Loading…
1
Increase memory limit for lean from 1G to 4G
#24 by butterthebuddha was merged May 17, 2020 Loading…
Allow displaying Lean goal in another frame
#23 by iocta was merged Mar 19, 2020 Loading…
1
feat(lean-input): update
#22 by fpvandoorn was merged Feb 11, 2020 Loading…
fix(lean-eri): require cl-lib
#21 by kritixilithos was merged Dec 29, 2019 Loading…
1
1
fix(lean-eri): remove runtime require of cl
#18 by bandali was merged Sep 14, 2019 Loading…
1
feat(lean-diff-types): take type diff from company-coq
#9 by cipher1024 was closed Sep 6, 2018 Loading…
3
fix(lean-info): lean-show-goal no longer interrupts `lean-find-defi…
#6 by cipher1024 was merged Jun 4, 2018 Loading…
5
Default to executable name "lean"
#5 by cdunham was merged Jun 3, 2018 Loading…
1
chore(README): clarifications
#2 by Kha was merged Oct 12, 2017 Loading…
1
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.