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 _ _ =>