summaryrefslogtreecommitdiff
path: root/examples
diff options
context:
space:
mode:
authorkrasimir <krasimir@chalmers.se>2010-10-13 17:53:44 +0000
committerkrasimir <krasimir@chalmers.se>2010-10-13 17:53:44 +0000
commit82214f0be5688ca55d0d89381be5daf3a9123903 (patch)
tree5869891ca4371bf08cbd0e6b83009fa6a76a88f7 /examples
parent95713b9489f412c2aa2892c1465ad7e2c66c1e95 (diff)
generalize the nqueens function in NQueens.gf
Diffstat (limited to 'examples')
-rw-r--r--examples/nqueens/NQueens.gf2
-rw-r--r--examples/nqueens/NQueensAscii.gf2
2 files changed, 2 insertions, 2 deletions
diff --git a/examples/nqueens/NQueens.gf b/examples/nqueens/NQueens.gf
index 960bef6d1..6eec8953f 100644
--- a/examples/nqueens/NQueens.gf
+++ b/examples/nqueens/NQueens.gf
@@ -6,7 +6,7 @@ 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 nqueens : (n : Nat) -> Matrix n -> S ;
data nilV : ({s} : Nat) -> ({c} : [Nat]) -> Vec s zero c ;
consV : ({l},j,k : Nat) ->
diff --git a/examples/nqueens/NQueensAscii.gf b/examples/nqueens/NQueensAscii.gf
index a5bb2ed76..489f5ce7b 100644
--- a/examples/nqueens/NQueensAscii.gf
+++ b/examples/nqueens/NQueensAscii.gf
@@ -3,7 +3,7 @@ concrete NQueensAscii of NQueens = NatAscii ** {
lincat S, Matrix, Vec = Str ;
ListNat, Sat = {} ;
-lin queens m = m ;
+lin nqueens _ m = m ;
lin nilV _ _ = "" ;
consV _ j k _ _ v = j ++ "X" ++ k ++ ";" ++ v ;