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

chore: fix typo

Browse source 
invalide -> invalid
This commit is contained in:
Reid Barton 2021-01-25 16:51:59 -05:00 • committed by Leonardo de Moura
parent d408c835d2
commit ccc09d9cbf
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/Meta/InferType.lean
View file

@ -95,7 +95,7 @@ private def inferConstType (c : Name) (us : List Level) : MetaM Expr := do
private def inferProjType (structName : Name) (idx : Nat) (e : Expr) : MetaM Expr := do
let failed {α} : Unit → MetaM α := fun _ =>
throwError! "invalide projection{indentExpr (mkProj structName idx e)}"
throwError! "invalid projection{indentExpr (mkProj structName idx e)}"
let structType ← inferType e
let structType ← whnf structType
matchConstStruct structType.getAppFn failed fun structVal structLvls ctorVal =>