All pull requests

Pull requests

• compress Json output to be on single line

  #144·FrederickPu opened Feb 4, 2026·

  ·

• Report errors in import statements

  #141·Kripner opened Dec 17, 2025·

  ·

• Add setOptions

  #130·augustepoiroux opened Sep 25, 2025Contributor·

  ·

• added ability to loadDynlib through command line flag

  #124·FrederickPu opened Jul 24, 2025·

  ·
  7

• make repl more extensible

  #121·Qiu233 opened Jul 15, 2025·

  ·

• Declaration information extraction

  #119·augustepoiroux opened Jul 9, 2025Contributor·

  ·

• update test scripts

  #117·RexWzh opened Jul 4, 2025Contributor·

  ·

• add removeProofState

  #111·shanjiaming opened Jun 29, 2025·

  ·

• Automated prefix state sharing optimization

  #110·augustepoiroux opened Jun 27, 2025Contributor·

  ·
  1

• Introduce incremental processing of the commands

  #109·augustepoiroux opened Jun 27, 2025Contributor·

  ·
  1

• Fix LocalContext and LocalInstance captured by sorries for the tactic mode

  #108·augustepoiroux opened Jun 27, 2025Contributor·

  ·
  1

• Command to get theorem type

  #101·sorgfresser opened May 7, 2025Contributor·

  ·
  2

• LeanDojo's REPL/ExtractData.lean and mods to REPL/Main.lean to populate AST

  awaiting-author
  #96·vadimkantorov opened May 1, 2025·

  ·
  1

• Add batch processing to LeanRepl

  #93·FrederickPu opened Apr 28, 2025·

  ·
  12

• Implement soft timeout option

  #92·augustepoiroux opened Apr 22, 2025Contributor·

  ·
  3

• Add Pantograph-like approach to tactic mode

  #90·augustepoiroux opened Apr 21, 2025Contributor·3 tasks·

  ·
  4

• Add proof step verification

  #85·Kripner opened Apr 16, 2025·

  ·
  1

• add garbage collection option

  awaiting-author
  #83·RexWzh opened Apr 10, 2025Contributor·

  ·
  26

• Python package

  #5·zhangir-azerbayev opened Apr 5, 2023·

  ·
  15