forked from GitHub/gf-core
split the testsuite to different directories for compiler, runtime and libraries
This commit is contained in:
34
testsuite/runtime/paraphrase/Nat.gf
Normal file
34
testsuite/runtime/paraphrase/Nat.gf
Normal file
@@ -0,0 +1,34 @@
|
||||
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) ;
|
||||
|
||||
fun plus' : Nat -> Nat -> Nat ;
|
||||
def plus' Zero = \y -> y ;
|
||||
def plus' (Succ x) = \y -> Succ (plus x y) ;
|
||||
|
||||
}
|
||||
Reference in New Issue
Block a user