From c30e9ca551a85fa8f7a0ce080bcc93ce0eb9ccd1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 21 Oct 2019 10:51:55 -0700
Subject: [PATCH] chore: add `TypeContext.lean` file

---
 library/Init/Lean/TypeContext.lean | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 library/Init/Lean/TypeContext.lean

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
+-/