Metadata-Version: 2.3
Name: lean-repl-py
Version: 0.1.6
Summary: A Python application to interact with the Lean REPL.
License: MIT
Author: Simon Sorg
Author-email: simonsorg13@gmail.com
Requires-Python: >=3.9,<4.0
Classifier: License :: OSI Approved :: MIT License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.9
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Requires-Dist: pydantic (>=2.10.3,<3.0.0)
Description-Content-Type: text/markdown

# lean-repl-py

**lean-repl-py** is a Python application designed to interact with the Lean REPL (Read-Eval-Print Loop). It provides an interface for sending commands to Lean and processing responses, making it easier to automate theorem proving using Python.

## Features

- **Simple Interface**: Send Lean commands and receive responses seamlessly.
- **Automation**: Useful for scripting Lean interactions programmatically.
- **No Dependencies**: A lightweight tool with zero external dependencies.
- **Fast**: Adds no noticeable overhead on top of the lean REPL.

## Installation

You can install `lean-repl-py` via [PyPI](https://pypi.org/):

```bash
pip install lean-repl-py
```

## Prerequisites
Requires `lake` to be available on your system. That's it, no more strings attached.

Importantly, lean-repl-py ships with the correct version of the lean repl, so it is not needed separately.

## Important notices

The first start in a new python environment will take some time, as the repl must be built first.

