examples/nqueens/Nat.gf


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

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) ;

}