Reimplementation of the Natural Number Game, in Rocq.
Run:
nix develop
Which provides Rocq 9.0.0, its stdlib and coq-lsp.
rocq makefile -f _RocqProject -o RocqMakefile
make -f RocqMakefile
- Remove
Parameterblocks inGame/Natural.vand implement your ownnaturalnumber type and its operations. - Go and solve the problems in each world.