summaryrefslogtreecommitdiff
path: root/examples/test/paraphrase/Nat.gf
diff options
context:
space:
mode:
authoraarne <aarne@cs.chalmers.se>2008-10-14 11:20:44 +0000
committeraarne <aarne@cs.chalmers.se>2008-10-14 11:20:44 +0000
commita2e3b1ce73c46997ce4934ad76ed67efa93a649e (patch)
tree2417a302d5b807be9d32627bfb95e0dc049ea17d /examples/test/paraphrase/Nat.gf
parenta11f1b14370883b903da5b93de88984a3cfb9344 (diff)
moved paraphrases to examples/test/, meant for small grammars used for testing various aspects
Diffstat (limited to 'examples/test/paraphrase/Nat.gf')
-rw-r--r--examples/test/paraphrase/Nat.gf29
1 files changed, 29 insertions, 0 deletions
diff --git a/examples/test/paraphrase/Nat.gf b/examples/test/paraphrase/Nat.gf
new file mode 100644
index 000000000..7caa0fc93
--- /dev/null
+++ b/examples/test/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) ;
+}