even simpler version of NQueens

4 files changed, 5 insertions, 11 deletions

diff --git a/examples/nqueens/NQueens.gf b/examples/nqueens/NQueens.gf
index bcef1db5c..ba8a4e109 100644
--- a/examples/nqueens/NQueens.gf
+++ b/examples/nqueens/NQueens.gf
@@ -6,7 +6,9 @@ cat Vec (s,l : Nat) Constr ;
 cat Sat Nat Nat Constr ;
 
 data nilV  : (s : Nat) -> (c : Constr) -> Vec s zero c ;
-     consV : (s,l,j : Nat) -> (c : Constr) -> LT j s -> Sat j (succ zero) c -> Vec s l (consC j c) -> Vec s (succ l) 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 ;
 
      nilC  : Constr ;
      consC : (j : Nat) -> Constr -> Constr ;
diff --git a/examples/nqueens/NQueensAscii.gf b/examples/nqueens/NQueensAscii.gf
index 6a2c6f442..0af99435a 100644
--- a/examples/nqueens/NQueensAscii.gf
+++ b/examples/nqueens/NQueensAscii.gf
@@ -4,7 +4,7 @@ lincat Matrix, Vec = Str ;
        Constr, Sat = {} ;
 
 lin nilV _ _ = "" ;
-    consV _ _ f _ l _ v = f ++ "X" ++ l ++ "\n" ++ v ;
+    consV _ j k _ _ v = j ++ "X" ++ k ++ "\n" ++ v ;
 
     matrix _ v = v ;
 
diff --git a/examples/nqueens/Nat.gf b/examples/nqueens/Nat.gf
index d53dc10ac..638fb277c 100644
--- a/examples/nqueens/Nat.gf
+++ b/examples/nqueens/Nat.gf
@@ -6,15 +6,11 @@ data zero : Nat ;
      succ : Nat -> Nat ;
 
 cat NE (i,j : Nat) ;
-cat LT (i,j : Nat) ;
 
 data zNE : (i,j : Nat) -> NE i j -> NE (succ i) (succ j) ;
      lNE : (j : Nat) -> NE zero (succ j) ;
      rNE : (j : Nat) -> NE (succ j) zero ;
 
-     zLT : (n : Nat) -> LT zero (succ n) ;
-     sLT : (m,n : Nat) -> LT m n -> LT (succ m) (succ n) ;
-
 fun plus : Nat -> Nat -> Nat ;
 def plus zero     n = n ;
     plus (succ m) n = succ (plus m n) ;
diff --git a/examples/nqueens/NatAscii.gf b/examples/nqueens/NatAscii.gf
index 5c0892d66..86ffa923f 100644
--- a/examples/nqueens/NatAscii.gf
+++ b/examples/nqueens/NatAscii.gf
@@ -5,10 +5,6 @@ lincat Nat = Str ;
 lin zero   = "" ;
     succ n = "_" ++ n ;
 
-lincat LT = Str ;
-       NE = {} ;
-
-lin zLT n = n ;
-    sLT _ _ l = l ;
+lincat NE = {} ;
 
 }
\ No newline at end of file