Skip to content

Pull requests: leanprover-community/lean

New pull request New
25 Open 585 Closed
25 Open 585 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: use reducible transparency when producing no_confusion_type and injectivity lemmas awaiting-review
#812 opened Jun 14, 2023 by eric-wieser Loading…
10
fix: use a less ambiguous encoding for relative imports
#811 opened May 25, 2023 by digama0 Loading…
fix(frontends/lean/parser): start positions of trailing parser (NuD) nodes
#785 opened Nov 18, 2022 by digama0 Loading…
2
feat(frontends/lean/pp): use forall notation for all pi types from a Type to a Prop awaiting-review
#770 opened Sep 19, 2022 by kmill Loading…
16
FreeBSD patches
#764 opened Sep 1, 2022 by yurivict Loading…
1
feat(simp_lemmas): allow user congr lemma to have fixed parameters
#709 opened Mar 28, 2022 by kmill Loading…
2
feat(elaborator,pp): improvements to dot notation
#708 opened Mar 26, 2022 by kmill Loading…
feat(frontends): local names in user-defined notation WIP Work in progress
#701 opened Mar 15, 2022 by b-mehta • Draft
Add module_info.get_all
#645 opened Nov 2, 2021 by eric-wieser Loading…
5
doc(library/init/meta/interactive): improve repeat documentation
#621 opened Sep 18, 2021 by BoltonBailey Loading…
2
fix(library/type_context): do not enfore semireducible transparency in implicit arguments
#556 opened Mar 17, 2021 by gebner • Draft
feat(library/init/core): allow lists of proofs
#533 opened Feb 18, 2021 by eric-wieser • Draft
6
feat(*): Log progress messages to stderr even when using json output on stdout
#495 opened Oct 29, 2020 by eric-wieser Loading…
2
fix(init/meta/converter/interactive): Do not allow rw to create ⊢ goals in conv mode WIP Work in progress
#475 opened Oct 8, 2020 by eric-wieser Loading…
5
doc(tactic): add explanation of approx for unify
#459 opened Sep 2, 2020 by EdAyers • Draft
1
feat(?): Better support for prod in well_founded
#414 opened Jul 28, 2020 by eric-wieser • Draft
1
feat(meta/environment): the equations that lead to a given definition are now accessible in Lean code
#393 opened Jul 16, 2020 by cipher1024 Loading…
5
assumption?
#281 opened May 27, 2020 by jalex-stark Loading…
25
feat(library/init/meta/format): has_to_format α implies has_to_string α
#231 opened May 12, 2020 by JLimperg Loading…
1
chore(library/init/data): constructive nat
#171 opened Apr 1, 2020 by Jack-Pumpkinhead Loading… Lean 3.12
4
feat(tactic/lint): add some hooks to allow linting of proof scripts WIP Work in progress
#168 opened Apr 1, 2020 by cipher1024 Loading…
1
Feature/vm dynload WIP Work in progress
#49 opened Jun 3, 2019 by cipher1024 Loading…
Add structs to FFI WIP Work in progress
#47 opened Jun 1, 2019 by agentultra • Draft
WIP: cwd in environment objects WIP Work in progress
#43 opened May 17, 2019 by cipher1024 Loading…
feat(init/data/cached): Caching mechanism [WIP] WIP Work in progress
#35 opened May 10, 2019 by digama0 Loading…
ProTip! What’s not been updated in a month: updated:<2024-10-12.