inductive Player : Type

• Proposer : Player
• Chooser : Player

@[reducible, inline]

abbrev Winner : Type

Equations

• Winner = Player

def winning_proposer (b : Bool) : Winner

Equations

• winning_proposer b = if b = true then Player.Proposer else Player.Chooser

def winning_chooser (b : Bool) : Winner

Equations

• winning_chooser b = if b = true then Player.Chooser else Player.Proposer

inductive Side : Type

• Left : Side
• Right : Side

@[reducible, inline]

abbrev PMoves (ℍ : Type) : Type

Equations

• PMoves ℍ = (ℍ × ℍ)

def PMoves.left {ℍ : Type} : PMoves ℍ → ℍ

Equations

• e.left = e.fst

def PMoves.right {ℍ : Type} : PMoves ℍ → ℍ

Equations

• e.right = e.snd

inductive ChooserPrimMoves (α : Type) : Type

• Now {α : Type} : ChooserPrimMoves α
• Continue {α : Type} (opts : α) : ChooserPrimMoves α

@[reducible, inline]

abbrev ChooserSmp : Type

Equations

• ChooserSmp = ChooserPrimMoves Unit

@[reducible, inline]

abbrev ChooserMoves : Type

Equations

• ChooserMoves = ChooserPrimMoves Side