Contributing
A Lean development shell is provided in the Nix flake. Nix usage is optional. Any contribution has to pass the pre-commit hooks:
pre-commit install --install-hooks
All commit messages must conform to the Conventional Commits specification.
Testing
The tests are based on LSpec. To run tests, use either
nix flake check
or
lake test
You can run an individual test by specifying a prefix
lake test -- Frontend/Collect
Formatting
When writing Lean code, follow the guidelines
- Functions should be in
camelCase - Theorems and tests should be in
snake_case - Write the
|in a pattern-matchingleton the next line. This is for visual distinction with long function arguments.
let .some result := function
| fail "incorrect"
- Each test should be pinpointed and devolatilized.