From 02ddbfa7da27e2105bf8ea11d6f138d32fbaff5c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 29 Dec 2019 09:49:55 -0800
Subject: [PATCH] fix: typo

---
 src/Init/Lean/Level.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Init/Lean/Level.lean b/src/Init/Lean/Level.lean
index a089ec17c4..262aab7309 100644
--- a/src/Init/Lean/Level.lean
+++ b/src/Init/Lean/Level.lean
@@ -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