From 6d7041fcb43d4a5d2d26d17b045557d9e8fc034c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 16 Sep 2019 18:30:35 -0700
Subject: [PATCH] test(tests/playground/inst): add `instantiate` and
 `instantiateRev` simple tests

---
 tests/playground/inst.lean | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 tests/playground/inst.lean

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 ()