文件名称：sudoku:数独游戏，您必须证明自己的推论是有效的
文件大小：572KB
文件格式：ZIP
更新时间：2024-06-07 19:07:29
Lean
在精益定理证明者中玩数独 如何开始玩 假设您通过g++拥有C ++编译器。 在Debian / Ubuntu上， sudo apt install build-essential应该可以解决问题。 首先，我们下载代码。 leanproject get TwoFx/sudoku 接下来，我们编译为我们生成关卡的程序。 cd sudoku g++ -std=gnu++11 -O2 scripts/gen.cpp -o gen 接下来，我们将使用它为我们生成一个关卡。 将数独输入到文件中（因为81个数字由空格分隔，所以0为空白）。 有关示例，请参见scripts/easy1 。 ./gen < your> src/play.lean 接下来，我们必须告诉Visual Studio代码不要使我们的代码超时。 这是必需的，因为我编写了效率很低且很慢的代码。
【文件预览】：
sudoku-master
----.gitignore(1KB)
----README.md(3KB)
----.github()
--------workflows()
----.vscode()
--------settings.json(271B)
----LICENSE(11KB)
----src()
--------basic.lean(10KB)
--------stactic.lean(13KB)
--------widget.lean(4KB)
----scripts()
--------easy1(163B)
--------gen.cpp(2KB)
----screenshot()
--------screenshot.jpg(628KB)
----leanpkg.toml(239B)