forked from GitHub/gf-core
add start category S in NQueens. This helps the EditorApp to find the start category
This commit is contained in:
@@ -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)
|
||||
|
||||
Reference in New Issue
Block a user