diff options
Diffstat (limited to 'testsuite/paraphrase/Nat.gf')
| -rw-r--r-- | testsuite/paraphrase/Nat.gf | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/testsuite/paraphrase/Nat.gf b/testsuite/paraphrase/Nat.gf new file mode 100644 index 000000000..7caa0fc93 --- /dev/null +++ b/testsuite/paraphrase/Nat.gf @@ -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) ; +} |
