max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: typo

Browse source
This commit is contained in:
Wojciech Nawrocki 2021-07-01 11:34:50 -07:00 • committed by Sebastian Ullrich
parent c7beb283e9
commit 522cbc16d9
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Environment.lean
View file

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