From 7ab79b8729825761f246630dcb7ceff34dec49ca Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Oct 2019 19:48:27 -0700
Subject: [PATCH] chore: missing instance

---
 library/Init/Lean/MetavarContext.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/library/Init/Lean/MetavarContext.lean b/library/Init/Lean/MetavarContext.lean
index 42c5f103e2..7f4fe1467b 100644
--- a/library/Init/Lean/MetavarContext.lean
+++ b/library/Init/Lean/MetavarContext.lean
@@ -16,6 +16,8 @@ structure MetavarContext :=
 
 namespace MetavarContext
 
+instance : Inhabited MetavarContext := ⟨{}⟩
+
 @[export lean_mk_metavar_ctx]
 def mkMetavarContext : Unit → MetavarContext :=
 fun _ => {}