diff --git a/tests/playground/arith_eval.ml b/tests/playground/arith_eval.ml
new file mode 100644
index 0000000000..9c6bb753db
--- /dev/null
+++ b/tests/playground/arith_eval.ml
@@ -0,0 +1,19 @@
+type expr =
+| Var of int
+| Val of int
+| Add of expr * expr;;
+
+let dec n =
+  if n == 0 then 0 else n - 1;;
+
+let rec mk_expr n v =
+  if n == 0 then Val v
+  else Add (mk_expr (n-1) (v+1), mk_expr (n-1) (dec v));;
+
+let rec eeval e =
+ match e with
+ | Val n -> n
+ | Var x -> 0
+ | Add (l, r) -> eeval l + eeval r;;
+
+Printf.printf "%8d\n" (eeval (mk_expr 26 1));;
diff --git a/tests/playground/arith_eval_nat.lean b/tests/playground/arith_eval_nat.lean
new file mode 100644
index 0000000000..a3554eba73
--- /dev/null
+++ b/tests/playground/arith_eval_nat.lean
@@ -0,0 +1,19 @@
+inductive Expr
+| Var : nat → Expr
+| Val : nat → Expr
+| Add : Expr → Expr → Expr
+
+open Expr nat
+
+def mk_expr : nat → nat → Expr
+| 0        v := Val v
+| (succ n) v := Add (mk_expr n (v+1)) (mk_expr n (v-1))
+
+def eval : Expr → nat
+| (Var x) := 0
+| (Val v) := v
+| (Add l r) := eval l + eval r
+
+def main : io uint32 :=
+io.println' (to_string $ eval (mk_expr 26 1)) *>
+pure 0
diff --git a/tests/playground/arith_eval_uint32.lean b/tests/playground/arith_eval_uint32.lean
new file mode 100644
index 0000000000..e78e69681e
--- /dev/null
+++ b/tests/playground/arith_eval_uint32.lean
@@ -0,0 +1,22 @@
+inductive Expr
+| Var : uint32 → Expr
+| Val : uint32 → Expr
+| Add : Expr → Expr → Expr
+
+open Expr
+
+def dec (n : uint32) : uint32 :=
+if n = 0 then 0 else n-1
+
+def mk_expr : uint32 → uint32 → Expr | n v :=
+if n = 0 then Val v
+else Add (mk_expr (n-1) (v+1)) (mk_expr (n-1) (dec v))
+
+def eval : Expr → uint32
+| (Var x) := 0
+| (Val v) := v
+| (Add l r) := eval l + eval r
+
+def main : io uint32 :=
+io.println' (to_string $ eval (mk_expr 26 1)) *>
+pure 0