From 83ae3b7aaa5dd66b9929afa29ab99367a0d233f4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 21 Dec 2020 07:09:57 -0800 Subject: [PATCH] fix: bug introduced when moving to new frontend --- src/Lean/Elab/Level.lean | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/src/Lean/Elab/Level.lean b/src/Lean/Elab/Level.lean index 6daa79ed3d..a2000ef206 100644 --- a/src/Lean/Elab/Level.lean +++ b/src/Lean/Elab/Level.lean @@ -45,18 +45,12 @@ partial def elabLevel (stx : Syntax) : LevelElabM Level := withRef stx do elabLevel (stx.getArg 1) else if kind == `Lean.Parser.Level.max then let args := stx.getArg 1 |>.getArgs - let mut lvl ← elabLevel args.back - for arg in args[:args.size-1] do - let arg ← elabLevel arg - lvl := mkLevelMax' lvl arg - return lvl + args[:args.size - 1].foldrM (init := ← elabLevel args.back) fun stx lvl => + return mkLevelMax' (← elabLevel stx) lvl else if kind == `Lean.Parser.Level.imax then let args := stx.getArg 1 |>.getArgs - let mut lvl ← elabLevel args.back - for arg in args[:args.size-1] do - let arg ← elabLevel arg - lvl := mkLevelIMax' lvl arg - return lvl + args[:args.size - 1].foldrM (init := ← elabLevel args.back) fun stx lvl => + return mkLevelIMax' (← elabLevel stx) lvl else if kind == `Lean.Parser.Level.hole then mkFreshLevelMVar else if kind == numLitKind then