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