diff --git a/library/Init/Lean/TypeContext.lean b/library/Init/Lean/TypeContext.lean
new file mode 100644
index 0000000000..0a3fa4e35a
--- /dev/null
+++ b/library/Init/Lean/TypeContext.lean
@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Expr
+
+
+/-
+Notes:
+- Track whether a metavariable assignment was used to enable caching.
+- Add TypeContextConfig type class
+-/