diff options
Diffstat (limited to 'examples/nqueens/NQueens.gf')
| -rw-r--r-- | examples/nqueens/NQueens.gf | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/examples/nqueens/NQueens.gf b/examples/nqueens/NQueens.gf index bd236bf55..960bef6d1 100644 --- a/examples/nqueens/NQueens.gf +++ b/examples/nqueens/NQueens.gf @@ -1,10 +1,13 @@ abstract NQueens = Nat ** { +cat S ; cat Matrix Nat ; cat [Nat] ; cat Vec (s,l : Nat) [Nat] ; cat Sat Nat Nat [Nat] ; +data queens : Matrix (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))) -> S ; + data nilV : ({s} : Nat) -> ({c} : [Nat]) -> Vec s zero c ; consV : ({l},j,k : Nat) -> let s = succ (plus j k) |