My attempts at a formalization of Hanabi in Lean.

Exact

Exact Union RegExp

Maximilian Keßler d60463024d directly give recursive function with proof		2025-11-23 01:47:33 +01:00
Hanabi	directly give recursive function with proof	2025-11-23 01:47:33 +01:00
.gitignore	move defs into separate file	2025-09-20 18:36:36 +02:00
Hanabi.lean	start with completion file: exhaust actions in games	2025-11-22 23:58:10 +01:00
lake-manifest.json	add lean metainfo on project	2025-09-23 13:22:13 +02:00
lakefile.toml	add lean metainfo on project	2025-09-23 13:22:13 +02:00
lean-toolchain	add lean metainfo on project	2025-09-23 13:22:13 +02:00
notes.txt	add notes on theorem	2025-09-23 13:22:36 +02:00