Skip to content

A simple REPL for Lean 4, returning information about errors and sorries.

Notifications You must be signed in to change notification settings

xinhjBrant/repl

 
 

Repository files navigation

A Read-Eval-Print Loop for Lean 4 with Enhanced Information Extraction Capabilities

This project is a fork of the leanprover-community/repl repository, augmented with additional features to support advanced information extraction. The enhancements are implemented in REPL/ExtractData.lean, which has been adapted from lean-dojo/LeanDojo.

To see an example of how these features can be utilized, refer to the files test/aime_1983_p9.in and test/aime_1983_p9.expected.out. These examples demonstrate the practical application and output of the enhanced information extraction capabilities.

About

A simple REPL for Lean 4, returning information about errors and sorries.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Lean 98.4%
  • Shell 1.6%