q.lean

import data.string.basic
import system.io

def unlines := string.intercalate "\n"
def unwords := string.intercalate " "

def range : ∀n, list (fin n)
| 0 := []
| (n+1) := (range n).map (λ⟨a, h⟩, ⟨a, h.step⟩) ++ [⟨n, nat.less_than_or_equal.refl⟩]

def board (size : ℕ) (α : Type) := ∀(x y : fin size), α

namespace board
  variables {size : ℕ} {α : Type}

  def empty : board size (option bool)
  | _ _ := none

  def place : board size α → fin size → fin size → α → board size α
  | b x y t x₁ y₁ := if x = x₁ ∧ y = y₁ then t else b x₁ y₁

  def to_string [has_to_string α] : board size α → string
  | b :=
    unlines $ flip list.map (range size) $ λy,
    unwords $ flip list.map (range size) $ λx,
    has_to_string.to_string (b x y)

  instance [has_to_string α] : has_to_string (board size α) := ⟨to_string⟩
end board

def main : io unit := do
  let b : board 3 (option bool) := board.empty,
  io.print_ln (b.place 0 1 (some true))

#eval main