Table of contents

This post details my efforts to construct a formally verified endgame tablebase generator for certain classes of two-player combinatorial games. You can view the code here. I generated a sample tablebase for a simple game known as a bear game, and made a small frontend where you can query this tablebase and play games against it here.

Cantor’s Theorem about dense linear orders states that any two linear orders which are

Oftentimes in programming, there will be a function that can obviously be generalized to an arbitrary number of arguments, and it would be convenient to be able to handle each of the generalized versions of this function in some sort of uniform manner.