module Logic.Square;
import Stdlib.Prelude open;
import Logic.Symbol open;
import Stdlib.Data.Nat.Ord open;
import Logic.Extra open;
--- A square is each of the holes in a board
type Square :=
| --- An empty square has a ;Nat; that uniquely identifies it
empty : Nat → Square
| --- An occupied square has a ;Symbol; in it
occupied : Symbol → Square;
--- Equality for ;Square;s
==Square : Square → Square → Bool
| (empty m) (empty n) := m == n
| (occupied s) (occupied t) := ==Symbol s t
| _ _ := false;
--- Textual representation of a ;Square;
showSquare : Square → String
| (empty n) := " " ++str natToString n ++str " "
| (occupied s) := " " ++str showSymbol s ++str " ";
replace (player : Symbol) (k : Nat) : Square → Square
| (empty n) := if (n Stdlib.Data.Nat.Ord.== k) (occupied player) (empty n)
| s := s;
Last modified on 2023-10-06 13:21 UTC