examples/test/paraphrase/Nat.gf


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

abstract Nat = {

cat Nat ;

data 
  Zero : Nat ;
  Succ : Nat -> Nat ;
  
fun one : Nat ;
def one = Succ Zero ;

fun plus : Nat -> Nat -> Nat ;
def plus x Zero = x ;
def plus x (Succ y) = Succ (plus x y) ;

fun twice : Nat -> Nat ;
def twice x = plus x x ;

fun times : Nat -> Nat -> Nat ;
def times x Zero = Zero ;
def times x (Succ y) = plus (times x y) x ;

fun four : Nat ;
def four = twice (twice one) ;

fun exp : Nat -> Nat ;
def exp Zero = one ;
def exp (Succ x) = twice (exp x) ;
}