forked from GitHub/gf-core
generalize the nqueens function in NQueens.gf
This commit is contained in:
@@ -6,7 +6,7 @@ cat [Nat] ;
|
|||||||
cat Vec (s,l : Nat) [Nat] ;
|
cat Vec (s,l : Nat) [Nat] ;
|
||||||
cat Sat Nat Nat [Nat] ;
|
cat Sat Nat Nat [Nat] ;
|
||||||
|
|
||||||
data queens : Matrix (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))) -> S ;
|
data nqueens : (n : Nat) -> Matrix n -> S ;
|
||||||
|
|
||||||
data nilV : ({s} : Nat) -> ({c} : [Nat]) -> Vec s zero c ;
|
data nilV : ({s} : Nat) -> ({c} : [Nat]) -> Vec s zero c ;
|
||||||
consV : ({l},j,k : Nat) ->
|
consV : ({l},j,k : Nat) ->
|
||||||
|
|||||||
@@ -3,7 +3,7 @@ concrete NQueensAscii of NQueens = NatAscii ** {
|
|||||||
lincat S, Matrix, Vec = Str ;
|
lincat S, Matrix, Vec = Str ;
|
||||||
ListNat, Sat = {} ;
|
ListNat, Sat = {} ;
|
||||||
|
|
||||||
lin queens m = m ;
|
lin nqueens _ m = m ;
|
||||||
|
|
||||||
lin nilV _ _ = "" ;
|
lin nilV _ _ = "" ;
|
||||||
consV _ j k _ _ v = j ++ "X" ++ k ++ ";" ++ v ;
|
consV _ j k _ _ v = j ++ "X" ++ k ++ ";" ++ v ;
|
||||||
|
|||||||
Reference in New Issue
Block a user