From 522cbc16d992feda68f58daa98ecbb843dde710b Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Thu, 1 Jul 2021 11:34:50 -0700 Subject: [PATCH] fix: typo --- src/Lean/Environment.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 8aeb8a2641..209c4ea06c 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -659,7 +659,7 @@ private def throwUnexpectedType {α} (typeName : Name) (constName : Name) : Exce This function is still unsafe because it cannot guarantee that `typeName` is in fact the name of the type `α`. -/ unsafe def evalConstCheck (α) (env : Environment) (opts : Options) (typeName : Name) (constName : Name) : ExceptT String Id α := match env.find? constName with - | none => throw ("unknow constant '" ++ toString constName ++ "'") + | none => throw ("unknown constant '" ++ toString constName ++ "'") | some info => match info.type with | Expr.const c _ _ =>