themattchan
themattchan
/ Game.v
Created
July 25, 2017 03:14
— forked from arthuraa/Game.v
Basic combinatorial game theory
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Require Import Coq.Lists.List. | |
| Open Scope bool_scope. | |
| (* This is a direct definition of CGTs, using just one inductive type | |
| instead of a pair of mutually-inductive types *) | |
| Inductive game := Game { | |
| left_moves : list game; | |
| right_moves : list game |