diff --git a/src/Lean/Elab/Level.lean b/src/Lean/Elab/Level.lean index 5acc198755..8eb5b1fa72 100644 --- a/src/Lean/Elab/Level.lean +++ b/src/Lean/Elab/Level.lean @@ -56,7 +56,9 @@ register_builtin_option maxUniverseOffset : Nat := { private def checkUniverseOffset [Monad m] [MonadError m] [MonadOptions m] (n : Nat) : m Unit := do let max := maxUniverseOffset.get (← getOptions) unless n <= max do - throwError "maximum universe level offset threshold ({max}) has been reached, you can increase the limit using option `set_option maxUniverseOffset `, but you are probably misusing universe levels since offsets are usually small natural numbers" + throwError m!"Universe level offset `{n}` exceeds maximum offset `{max}`" + ++ .note m!"This code is probably misusing universe levels, since they are usually small natural numbers. \ + If you are confident this is not the case, you can increase the limit using `set_option maxUniverseOffset `" partial def elabLevel (stx : Syntax) : LevelElabM Level := withRef stx do let kind := stx.getKind diff --git a/tests/lean/bigUnivOffsets.lean.expected.out b/tests/lean/bigUnivOffsets.lean.expected.out index 1b0e2dd5e9..9bd74a9126 100644 --- a/tests/lean/bigUnivOffsets.lean.expected.out +++ b/tests/lean/bigUnivOffsets.lean.expected.out @@ -1,2 +1,6 @@ -bigUnivOffsets.lean:1:12-1:21: error: maximum universe level offset threshold (32) has been reached, you can increase the limit using option `set_option maxUniverseOffset `, but you are probably misusing universe levels since offsets are usually small natural numbers -bigUnivOffsets.lean:5:13-5:25: error: maximum universe level offset threshold (32) has been reached, you can increase the limit using option `set_option maxUniverseOffset `, but you are probably misusing universe levels since offsets are usually small natural numbers +bigUnivOffsets.lean:1:12-1:21: error: Universe level offset `100000000` exceeds maximum offset `32` + +Note: This code is probably misusing universe levels, since they are usually small natural numbers. If you are confident this is not the case, you can increase the limit using `set_option maxUniverseOffset ` +bigUnivOffsets.lean:5:13-5:25: error: Universe level offset `10000000` exceeds maximum offset `32` + +Note: This code is probably misusing universe levels, since they are usually small natural numbers. If you are confident this is not the case, you can increase the limit using `set_option maxUniverseOffset `