diff options
Diffstat (limited to 'examples/nqueens/Nat.gf')
| -rw-r--r-- | examples/nqueens/Nat.gf | 6 |
1 files changed, 3 insertions, 3 deletions
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 |