Language Lean

Status

Alpha

Versions

3.7.2

Test Frameworks

None

Interactive Proof Editing Support

Unfortunately, the Codewars environment does not support the interactive development of Lean proofs. The current recommended method of solving a Kata is by copying the relevant code snippets onto your local machine and developing your solution locally.

Setting up your local environment

1. Install elan

2. Run pip3 install mathlibtools, with sudo if necessary

3. Run leanproject new kata. This automatically creates a Lean3 project in kata/ with the latest Lean3 community version (3.7.2 at the time of writing) and the corresponding pre-compiled mathlib

4. Populate kata/src/ with the following Lean files:

   • Preloaded.lean: The Preloaded section of the Kata
   • Solution.lean: Your solution to this Kata
   • SolutionTest.lean: The (Sample) Test Cases for this Kata

   You should not modify Preloaded.lean or SolutionTest.lean when developing your solution locally, since you are not allowed to modify them on Codewars upon submission. To test your submission, open your command line, cd to kata/src/ and run lean SolutionTest.lean. A passing solution should only see one or more of the following lines (in any order, appearing any number of times) printed out to the console:

   • no axioms
   • propext
   • quot.sound
   • classical.choice

Timeout

16 seconds

Packages

• mathlib

Services

None