diff options
| author | krasimir <krasimir@chalmers.se> | 2010-03-24 16:14:36 +0000 |
|---|---|---|
| committer | krasimir <krasimir@chalmers.se> | 2010-03-24 16:14:36 +0000 |
| commit | fdd68f90403b28f332909aa095c30c18588a1bd7 (patch) | |
| tree | 7a0cda72ac9494524afe36cd01494384a118e646 /examples/nqueens | |
| parent | 14f19b986591abd53d444c6f6f479ca21d8cafbf (diff) | |
the Plus predicate from NQueens is replaced with definition for function plus
Diffstat (limited to 'examples/nqueens')
| -rw-r--r-- | examples/nqueens/NQueens.gf | 4 | ||||
| -rw-r--r-- | examples/nqueens/Nat.gf | 6 | ||||
| -rw-r--r-- | examples/nqueens/NatAscii.gf | 1 |
3 files changed, 5 insertions, 6 deletions
diff --git a/examples/nqueens/NQueens.gf b/examples/nqueens/NQueens.gf index 04aa96a80..bcef1db5c 100644 --- a/examples/nqueens/NQueens.gf +++ b/examples/nqueens/NQueens.gf @@ -6,13 +6,13 @@ cat Vec (s,l : Nat) Constr ; cat Sat Nat Nat Constr ; data nilV : (s : Nat) -> (c : Constr) -> Vec s zero c ; - consV : (s,l : Nat) -> (j : Nat) -> (c : Constr) -> LT j s -> Sat j (succ zero) c -> Vec s l (consC j c) -> Vec s (succ l) 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 ; nilC : Constr ; consC : (j : Nat) -> Constr -> Constr ; nilS : (j,d : Nat) -> Sat j d nilC ; - consS : (i,j : Nat) -> (d,dj,di : Nat) -> (c : Constr) -> NE i j -> Plus d j dj -> Plus d i di -> NE i dj -> NE di j -> Sat j (succ d) c -> Sat j d (consC i c) ; + 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 nilC -> Matrix s ; diff --git a/examples/nqueens/Nat.gf b/examples/nqueens/Nat.gf index 8c8b5d542..d53dc10ac 100644 --- a/examples/nqueens/Nat.gf +++ b/examples/nqueens/Nat.gf @@ -7,7 +7,6 @@ data zero : 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) ; @@ -16,7 +15,8 @@ data zNE : (i,j : Nat) -> NE i j -> NE (succ i) (succ j) ; 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) ; +fun plus : Nat -> Nat -> Nat ; +def plus zero n = n ; + plus (succ m) n = succ (plus m n) ; }
\ No newline at end of file diff --git a/examples/nqueens/NatAscii.gf b/examples/nqueens/NatAscii.gf index 26f6533ea..5c0892d66 100644 --- a/examples/nqueens/NatAscii.gf +++ b/examples/nqueens/NatAscii.gf @@ -7,7 +7,6 @@ lin zero = "" ; lincat LT = Str ; NE = {} ; - Plus = {} ; lin zLT n = n ; sLT _ _ l = l ; |