diff --git a/examples/nary.mcl b/examples/nary.mcl
new file mode 100644
index 00000000..6feaaf4b
--- /dev/null
+++ b/examples/nary.mcl
@@ -0,0 +1,49 @@
+(* main body *)
+(
+  fun (Nary : forall (n : Nat) -> Type@0)
+      (appNary : forall (n : Nat) (f : Nary (succ n)) (arg : Nat) -> Nary n)
+      (toNat : forall (f : Nary 0) -> Nat)
+      (n : Nat)
+      (f : Nary n)
+    -> (rec n return y -> (forall (g : Nary y) -> Nat)
+       | zero => toNat
+       | succ m, r => fun (g : Nary (succ m)) -> r (appNary m g (succ m))
+       end) f
+)
+(* Nary definition *)
+(
+  fun (n : Nat)
+    -> rec n return y -> Type@0
+       | zero => Nat
+       | succ m, r => forall (a : Nat) -> r
+       end
+)
+(* appNary definition *)
+(
+  fun (n : Nat)
+      (f : rec succ n return y -> Type@0
+           | zero => Nat
+           | succ m, r => forall (a : Nat) -> r
+           end)
+      (arg : Nat)
+    -> f arg
+)
+(* toNat definition *)
+(fun (f : Nat) -> f)
+(* arguments n and f
+
+   This function sums up all its 3 inputs.
+*)
+3
+(
+  (fun (add : forall (a : Nat) (b : Nat) -> Nat) -> (fun (a : Nat) (b : Nat) (c : Nat) -> add a (add b c)))
+  (
+    fun (a : Nat)
+        (b : Nat)
+      -> rec a return y -> Nat
+         | zero => b
+         | succ m, r => succ r
+         end
+  )
+)
+: Nat
diff --git a/examples/simple_nat.mcl b/examples/simple_nat.mcl
new file mode 100644
index 00000000..43e6251b
--- /dev/null
+++ b/examples/simple_nat.mcl
@@ -0,0 +1 @@
+succ 3 : Nat