My canonical solution for solving a Sudoku in Sentient

sudoku.snt

function main () {
  array9<array9<int5>> sudoku;

  sudoku.each(function (row) {
    invariant row.uniq?;

    invariant row.all?(function (n) {
      return n.between?(1, 9);
    });
  });

  sudoku.transpose.each(function (column) {
    invariant column.uniq?;
  });

  sudoku.boxes.each(function (box) {
    invariant box.uniq?;
  });

  expose sudoku;
};

function boxes (sudoku) {
  boxes = [];

  3.times(function^ (i) {
    3.times(function^ (j) {
      boxes.push(sudoku.box(i, j));
    });
  });

  return boxes;
};

function box (sudoku, i, j) {
  cells = [];

  x = i * 3;
  y = j * 3;

  3.times(function^ (i) {
    3.times(function^ (j) {
      cells = cells.push(sudoku[x + i][y + j]);
    });
  });

  return cells;
};

main();