From 07254fc71bee2cdf648952665ee8546f64d82fb0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 12 Oct 2020 15:57:39 -0700
Subject: [PATCH] fix: `checkIsDefinition`

For '[inline] partial' definitions in mutual blocks.
---
 src/Lean/Compiler/Util.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Compiler/Util.lean b/src/Lean/Compiler/Util.lean
index 491d3761c4..44e785163c 100644
--- a/src/Lean/Compiler/Util.lean
+++ b/src/Lean/Compiler/Util.lean
@@ -78,9 +78,10 @@ private def getDeclNamesForCodeGen : Declaration → List Name
 
 def checkIsDefinition (env : Environment) (n : Name) : Except String Unit :=
 match env.find? n with
-| (some (ConstantInfo.defnInfo _)) => Except.ok ()
-| none => Except.error "unknow declaration"
-| _    => Except.error "declaration is not a definition"
+| (some (ConstantInfo.defnInfo _))   => Except.ok ()
+| (some (ConstantInfo.opaqueInfo _)) => Except.ok ()
+| none => Except.error ("unknow declaration '" ++ toString n ++ "'")
+| _    => Except.error ("declaration is not a definition '" ++ toString n ++ "'")
 
 /--
   We generate auxiliary unsafe definitions for regular recursive definitions.