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:
Leonardo de Moura 2019-12-29 09:49:55 -08:00
parent b7218dad9d
commit 02ddbfa7da
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Lean/Level.lean
View file

@ -415,8 +415,8 @@ mkLevelIMax newLhs newRhs
@[inline] def updateIMax! (lvl : Level) (newLhs : Level) (newRhs : Level) : Level :=
match lvl with
| max lhs rhs d => updateIMax (imax lhs rhs d) newLhs newRhs rfl
| _ => panic! "imax level expected"
| imax lhs rhs d => updateIMax (imax lhs rhs d) newLhs newRhs rfl
| _ => panic! "imax level expected"
@[specialize] def instantiateParams (s : Name → Option Level) : Level → Level
| u@(zero _) => u