Knight's tour example

gistfile1.txt

// Knight's tour: Find the sequence of moves of a knight on a chessboard such that the knight visits every square exactly once. 

// A move is an array of 2 numbers indicating how many [rows, columns] a piece travels.
type Move: [Integer, 2]

// <static type> identifier : (<dependent types>) = <value>
let knightMoves: [Move] = [[2, 1], [1, 2], [-1, 2], [-2, 1], [-2, -1], [-1, -2], [1, -2], [2, -1]]

// A Position is a 2 element array indicating [row, column] index (in range 0 to 8) on the board.
type Position: [Integer 0...8, 2]

// Check whether a move from start to end is a valid knight's move. start-end does elementwise subtraction.
fn isKnightMove(start: Position, end: Position) Boolean : start - end in knightMoves   // start-end does an elementwise subtraction
fn knightsMoves(positions: [Position]) Boolean : all(map(isKnightMove, pairwise(positions)))
fn distinctMoves(positions: [Position]) Boolean : set(positions).length == positions.length

type Tour: [Position] knightsMoves distinctMoves

// Now that we know how to check whether a tour is valid, we can ask the runtime to generate a valid tour starting from 0, 0
// The types encode the logic and relationship between elements and are enumerable.
let tour: Tour = [[0, 0], ...]