Simpleafier
Simpleafier is a command line tool to help improve the quality of Lean code by converting any simp to simp only. This can help make Lean proofs more robust and maintainable by restricting the set of lemmas used by simp.
Requirements
- Python 3.6+
- Lean 4
lakemust be installed and available in your PATH.
Installation
Simpleafier is available on PyPI and can be installed using pip.
python -m pip install Simpleafier
Usage
To convert all simp calls in a Lean file to simp only:
python -m simpleafier path/to/your/file.lean --simponly --fast
simpleafier must be invoked from the root of your lake project. The lean file provided must be compilable without any errors. simpleafier will create a temporary file in the same directory as the original file for processing. At the end of the process, the temporary file will be deleted and the original file will be replaced with the modified version.
The --fast flag provides significantly faster processing, but may result in less accurate results that may need more manual fixes. However it is currently the recommended mode for using simpleafier as it is more stable and gives reasonably good results.
License
This project is licensed under the MIT License.
Contributing
Contributions, bug reports, and feature requests are welcome! Please open an issue or submit a pull request on GitHub.
1 maintainer
Metadata
1 maintainer
Release files for Simpleafier 0.1.4
For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.
Source distribution (sdist)
| File | Size | Uploaded | Provenance | |
|---|---|---|---|---|
| simpleafier-0.1.4.tar.gz | 5.6 kB | Without provenance | Details |
Built distribution (wheel)
| File | Interpreter | ABI | Platform | Reset |
|---|---|---|---|---|
| simpleafier-0.1.4-py3-none-any.whl | Python 3 | none | any | Details |
Total release size: 11.7 kB
Release files / simpleafier-0.1.4.tar.gz
| Download URL | simpleafier-0.1.4.tar.gz |
|---|---|
| Size | 5.6 kB |
| Tags | Source |
|
SHA-256 checksum How to use checksums |
499c4e8b880ee157ff3754de3aa0354301722a18ff116e0dc883f4ba4ae114e7
|
|
BLAKE2b-256 checksum How to use checksums |
e77c2c02378e611eb8b7dd911a80c1a32a5dd950d900b702f8816d5ffdbbb16c
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
No |
| Uploaded via |
twine/6.0.1 CPython/3.13.3
|
Release files / simpleafier-0.1.4-py3-none-any.whl
| Download URL | simpleafier-0.1.4-py3-none-any.whl |
|---|---|
| Size | 6.2 kB |
| Tags | Python 3 |
|
SHA-256 checksum How to use checksums |
e7606bdc034e0c2e81df861e875e48c8a0c3d3b1925213e2b84826e8afa52ee5
|
|
BLAKE2b-256 checksum How to use checksums |
fd6c0c8cb917b9305862907498de35b92c6adea6d6813219f9fada1a507a4db5
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
No |
| Uploaded via |
twine/6.0.1 CPython/3.13.3
|
Security for Simpleafier 0.1.4
Provenance
Provenance describes where a file came from. On PyPI, provenance is shared via attestations, which provide a verifiable record of the build or publishing details. View details, limitations and caveats.
No provenance found
None of the files in this release were uploaded with provenance metadata.
A note on package security
PyPI is a repository for distributing packages, not a service for auditing them. While third-party security researchers and our staff do their best to detect and remove malicious packages, PyPI cannot guarantee the quality, security or suitability of any given package.
To learn more about protecting yourself from malicious actors, visit our package security documentation.
