--- This module defines the ;Symbol; type and some helper functions.
module Logic.Symbol;

open import Stdlib.Prelude;

--- A symbol represents a token that can be placed in a square
type Symbol :=
  | --- The circle token
    O : Symbol
  | --- The cross token
    X : Symbol;

--- Equality for ;Symbol;s
==Symbol : Symbol → Symbol → Bool;
==Symbol O O := true;
==Symbol X X := true;
==Symbol _ _ := false;

--- Turns ;O; into ;X; and ;X; into ;O;
switch : Symbol → Symbol;
switch O := X;
switch X := O;

--- Textual representation of a ;Symbol;
showSymbol : Symbol → String;
showSymbol O := "O";
showSymbol X := "X";