programgames/sudoku/sudoku.xtl

source · imports s: games/sudoku/SudokuGrid.xtl

g : Int

value · line 8

g ← 1 s̲elect ˢp̲uzzles @

Used in: games/sudoku/sudoku.xtl:9, games/sudoku/sudoku.xtl:10, c, games/sudoku/sudoku.xtl:28, games/sudoku/sudoku.xtl:30, games/sudoku/sudoku.xtl:31

U : Int

value · line 13

U ← ˢu̲nits @

Used in: games/sudoku/sudoku.xtl:14, games/sudoku/sudoku.xtl:15

c : Int

value · line 20

c ← ˢc̲andidates g

Used in: games/sudoku/sudoku.xtl:21, games/sudoku/sudoku.xtl:22, games/sudoku/sudoku.xtl:24

h : Int

value · line 35

h ← 2 s̲elect ˢp̲uzzles @

Used in: games/sudoku/sudoku.xtl:36, games/sudoku/sudoku.xtl:37, games/sudoku/sudoku.xtl:38

k : Int

value · line 41

k ← 4 s̲elect ˢp̲uzzles @

Used in: games/sudoku/sudoku.xtl:42, x, ok

x : Int

value · line 46

x ← ˢs̲olve k

Used in: games/sudoku/sudoku.xtl:47, games/sudoku/sudoku.xtl:49, ok

s : Int

value · line 53

s ← ˢn̲ew 1

Used in: games/sudoku/sudoku.xtl:54, games/sudoku/sudoku.xtl:55, games/sudoku/sudoku.xtl:56

ok : Unit

value · line 61

ok ← "'& r_/ (k = 0) | x = k" a̲ssert< "the solution keeps every given"

a̲ssert< expands to

({ @ → ('∧ r̲/ (k = 0) ∨ x = k) ? @◆ ⎕E̲RR "assertion failed: '& r_/ (k = 0) | x = k (the solution keeps every given) [games/sudoku/sudoku.xtl:61]"◆ @ } @)

ok : Unit

value · line 62

ok ← "'& r_/ r_avel 1 = s:p_erUnit s:o_nehot x" a̲ssert< "every unit holds every digit once"

a̲ssert< expands to

({ @ → ('∧ r̲/ r̲avel 1 = ˢp̲erUnit ˢo̲nehot x) ? @◆ ⎕E̲RR "assertion failed: '& r_/ r_avel 1 = s:p_erUnit s:o_nehot x (every unit holds every digit once) [games/sudoku/sudoku.xtl:62]"◆ @ } @)