4 files changed, 0 insertions, 64 deletions
diff --git a/examples/nqueens/NQueens.gf b/examples/nqueens/NQueens.gf
deleted file mode 100644
index 6eec8953f..000000000
--- a/examples/nqueens/NQueens.gf
+++ /dev/null
@@ -1,21 +0,0 @@
-abstract NQueens = Nat ** {
-
-cat S ;
-cat Matrix Nat ;
-cat [Nat] ;
-cat Vec (s,l : Nat) [Nat] ;
-cat Sat Nat Nat [Nat] ;
-
-data nqueens : (n : Nat) -> Matrix n -> S ;
-
-data nilV  : ({s} : Nat) -> ({c} : [Nat]) -> Vec s zero c ;
-     consV : ({l},j,k : Nat) -> 
-                let s = succ (plus j k)
-                in ({c} : [Nat]) -> Sat j (succ zero) c -> Vec s l (ConsNat j c) -> Vec s (succ l) c ;
-
-     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) ;
-
-     matrix : ({s} : Nat) -> Vec s s BaseNat -> Matrix s ;
-
-}
diff --git a/examples/nqueens/NQueensAscii.gf b/examples/nqueens/NQueensAscii.gf
deleted file mode 100644
index 489f5ce7b..000000000
--- a/examples/nqueens/NQueensAscii.gf
+++ /dev/null
@@ -1,13 +0,0 @@
-concrete NQueensAscii of NQueens = NatAscii ** {
-
-lincat S, Matrix, Vec = Str ;
-       ListNat, Sat = {} ;
-
-lin nqueens _ m = m ;
-
-lin nilV _ _ = "" ;
-    consV _ j k _ _ v = j ++ "X" ++ k ++ ";" ++ v ;
-
-    matrix _ v = v ;
-
-}
diff --git a/examples/nqueens/Nat.gf b/examples/nqueens/Nat.gf
deleted file mode 100644
index d80d462b5..000000000
--- a/examples/nqueens/Nat.gf
+++ /dev/null
@@ -1,18 +0,0 @@
-abstract Nat = {
-
-cat Nat ;
-
-data zero : Nat ;
-     succ : Nat -> Nat ;
-
-cat NE (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 ;
-
-oper 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
deleted file mode 100644
index 7c4e1289b..000000000
--- a/examples/nqueens/NatAscii.gf
+++ /dev/null
@@ -1,12 +0,0 @@
-concrete NatAscii of Nat = {
-
-lincat Nat = Str ;
-
-lin zero   = "" ;
-    succ n = "-" ++ n ;
-
-lincat NE = {} ;
-
-lin plus x y = x ++ y ;
-
-}