Safe points field implementation in Lean
| Points | ||
| .editorconfig | ||
| .envrc | ||
| .gitignore | ||
| Bench.lean | ||
| flake.lock | ||
| flake.nix | ||
| lake-manifest.json | ||
| lakefile.lean | ||
| lean-toolchain | ||
| LICENSE.txt | ||
| Points.lean | ||
| README.md | ||
Points Game Field Implementation in Lean
Benchmark
To build bench you will need to install dependencies with:
MATHLIB_NO_CACHE_ON_UPDATE=1 lake update
Build with:
lake build bench
Run with:
time ./.lake/build/bin/bench --width 39 --height 32 --games-number 1000 --seed 7