paraphrase works a little better now ; added examples/paraphrase for testing

This commit is contained in:
aarne
2008-10-14 11:19:30 +00:00
parent e94f1cf2c7
commit df08e52d5c
5 changed files with 86 additions and 8 deletions

View File

@@ -0,0 +1,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) ;
}