update NQueens to use: 1) lists i.e. [Nat]; 2) implicit arguments

2 files changed, 12 insertions, 15 deletions

diff --git a/examples/nqueens/NQueens.gf b/examples/nqueens/NQueens.gf
index ba8a4e109..bd236bf55 100644
--- a/examples/nqueens/NQueens.gf
+++ b/examples/nqueens/NQueens.gf
@@ -1,21 +1,18 @@
 abstract NQueens = Nat ** {
 
 cat Matrix Nat ;
-cat Constr ;
-cat Vec (s,l : Nat) Constr ;
-cat Sat Nat Nat Constr ;
+cat [Nat] ;
+cat Vec (s,l : Nat) [Nat] ;
+cat Sat Nat Nat [Nat] ;
 
-data nilV  : (s : Nat) -> (c : Constr) -> Vec s zero c ;
-     consV : (l,j,k : Nat) -> 
+data nilV  : ({s} : Nat) -> ({c} : [Nat]) -> Vec s zero c ;
+     consV : ({l},j,k : Nat) -> 
                 let s = succ (plus j k)
-                in (c : Constr) -> Sat j (succ zero) c -> Vec s l (consC j c) -> Vec s (succ l) c ;
+                in ({c} : [Nat]) -> Sat j (succ zero) c -> Vec s l (ConsNat j c) -> Vec s (succ l) c ;
 
-     nilC  : Constr ;
-     consC : (j : Nat) -> Constr -> Constr ;
+     nilS : ({j,d} : Nat) -> Sat j d BaseNat ;
+     consS : ({i,j,d} : Nat) -> ({c} : [Nat]) -> NE i j -> NE i (plus d j) -> NE (plus d i) j -> Sat j (succ d) c -> Sat j d (ConsNat i c) ;
 
-     nilS : (j,d : Nat) -> Sat j d nilC ;
-     consS : (i,j,d : Nat) -> (c : Constr) -> NE i j -> NE i (plus d j) -> NE (plus d i) j -> Sat j (succ d) c -> Sat j d (consC i c) ;
+     matrix : ({s} : Nat) -> Vec s s BaseNat -> Matrix s ;
 
-     matrix : (s : Nat) -> Vec s s nilC -> Matrix s ;
-
-}
\ No newline at end of file
+}
diff --git a/examples/nqueens/NQueensAscii.gf b/examples/nqueens/NQueensAscii.gf
index 0af99435a..fabcd3c64 100644
--- a/examples/nqueens/NQueensAscii.gf
+++ b/examples/nqueens/NQueensAscii.gf
@@ -1,11 +1,11 @@
 concrete NQueensAscii of NQueens = NatAscii ** {
 
 lincat Matrix, Vec = Str ;
-       Constr, Sat = {} ;
+       ListNat, Sat = {} ;
 
 lin nilV _ _ = "" ;
     consV _ j k _ _ v = j ++ "X" ++ k ++ "\n" ++ v ;
 
     matrix _ v = v ;
 
-}
\ No newline at end of file
+}