From f4574a4cfa97e8f501967cf86f33beaf105d0497 Mon Sep 17 00:00:00 2001 From: krasimir Date: Sun, 21 Mar 2010 19:01:57 +0000 Subject: the NQueens algorithm written in GF --- examples/nqueens/Nat.gf | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 examples/nqueens/Nat.gf (limited to 'examples/nqueens/Nat.gf') diff --git a/examples/nqueens/Nat.gf b/examples/nqueens/Nat.gf new file mode 100644 index 000000000..8c8b5d542 --- /dev/null +++ b/examples/nqueens/Nat.gf @@ -0,0 +1,22 @@ +abstract Nat = { + +cat Nat ; + +data zero : Nat ; + succ : Nat -> Nat ; + +cat NE (i,j : Nat) ; +cat LT (i,j : Nat) ; +cat Plus Nat Nat 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) ; + + zP : (n : Nat) -> Plus zero n n ; + sP : (m,n,s : Nat) -> Plus m n s -> Plus (succ m) n (succ s) ; + +} \ No newline at end of file -- cgit v1.2.3