Skip to content

Pull requests: leanprover-community/repl

New pull request New
17 Open 74 Closed
17 Open 74 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
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

added ability to loadDynlib through command line flag
#124 opened Jul 24, 2025 by FrederickPu Loading…
7
make repl more extensible
#121 opened Jul 15, 2025 by Qiu233 Loading…
Declaration information extraction
#119 opened Jul 9, 2025 by augustepoiroux • Draft
update test scripts
#117 opened Jul 4, 2025 by RexWzh Loading…
add removeProofState
#111 opened Jun 29, 2025 by shanjiaming Loading…
Automated prefix state sharing optimization
#110 opened Jun 27, 2025 by augustepoiroux Loading…
1
Introduce incremental processing of the commands
#109 opened Jun 27, 2025 by augustepoiroux Loading…
1
Fix LocalContext and LocalInstance captured by sorries for the tactic mode
#108 opened Jun 27, 2025 by augustepoiroux Loading…
1
Command to get theorem type
#101 opened May 7, 2025 by sorgfresser • Draft
2
LeanDojo's REPL/ExtractData.lean and mods to REPL/Main.lean to populate AST awaiting-author
#96 opened May 1, 2025 by vadimkantorov Loading…
1
Add batch processing to LeanRepl
#93 opened Apr 28, 2025 by FrederickPu • Draft
12
Implement soft timeout option
#92 opened Apr 22, 2025 by augustepoiroux • Draft
1
Add Pantograph-like approach to tactic mode
#90 opened Apr 21, 2025 by augustepoiroux • Draft
3 tasks
4
[WIP] Add proof step verification.
#85 opened Apr 16, 2025 by Kripner Loading…
add garbage collection option awaiting-author
#83 opened Apr 10, 2025 by RexWzh Loading…
26
Report errors in import statements. awaiting-author
#73 opened Feb 17, 2025 by Kripner Loading…
1
Python package
#5 opened Apr 5, 2023 by zhangir-azerbayev • Draft
15
ProTip! no:milestone will show everything without a milestone.