diff --git a/tests/playground/inst.lean b/tests/playground/inst.lean
new file mode 100644
index 0000000000..b7aeeca584
--- /dev/null
+++ b/tests/playground/inst.lean
@@ -0,0 +1,16 @@
+import init.lean.expr
+open Lean
+
+def main (xs : List String) : IO Unit :=
+do
+let f := mkConst `f;
+let x := Expr.bvar 0;
+let y := Expr.bvar 1;
+let t := Expr.app (Expr.app (Expr.app f x) y) x;
+let a := mkConst `a;
+let b := Expr.app f (mkConst `b);
+IO.println t.dbgToString;
+IO.println (t.instantiate [a, b].toArray).dbgToString;
+IO.println (t.instantiateRev [a, b].toArray).dbgToString;
+IO.println (t.instantiate [a].toArray).dbgToString;
+pure ()