From cf17fbb8e9ef0af576b2d1a497035f3cbfe3107d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 4 Nov 2019 03:59:39 -0800
Subject: [PATCH] chore: missing `@[specialize]`

---
 library/Init/Lean/TypeUtil.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/Init/Lean/TypeUtil.lean b/library/Init/Lean/TypeUtil.lean
index 9cbd5f330a..b88d24eabe 100644
--- a/library/Init/Lean/TypeUtil.lean
+++ b/library/Init/Lean/TypeUtil.lean
@@ -152,7 +152,7 @@ else
   if args.size < 2 then e
   else mkAppRange (args.get! 1) 2 args.size args
 
-private def deltaBetaDefinition {α} (c : ConstantInfo) (lvls : List Level) (revArgs : Array Expr) (failK : Unit → α) (successK : Expr → α) : α :=
+@[specialize] private def deltaBetaDefinition {α} (c : ConstantInfo) (lvls : List Level) (revArgs : Array Expr) (failK : Unit → α) (successK : Expr → α) : α :=
 if c.lparams.length != lvls.length then failK ()
 else
   let val := c.instantiateValueLevelParams lvls;