From 04417fafe801a4b1a31dac696cb6a01d07c646b6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 26 Nov 2019 07:21:03 -0800
Subject: [PATCH] chore: add missing instance

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

diff --git a/src/Init/Lean/Expr.lean b/src/Init/Lean/Expr.lean
index 59454edce9..66599ffc91 100644
--- a/src/Init/Lean/Expr.lean
+++ b/src/Init/Lean/Expr.lean
@@ -52,6 +52,8 @@ def BinderInfo.hash : BinderInfo → USize
 
 instance BinderInfo.hashable : Hashable BinderInfo := ⟨BinderInfo.hash⟩
 
+instance BinderInfo.inhabited : Inhabited BinderInfo := ⟨BinderInfo.default⟩
+
 def BinderInfo.isInstImplicit : BinderInfo → Bool
 | BinderInfo.instImplicit => true
 | _                       => false