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

chore: fix parameter

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-13 09:14:46 -07:00
parent c24ff8fe16
commit 5103040063
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/Lean/Elab/Log.lean
View file

@ -66,10 +66,10 @@ log stx MessageSeverity.warning msgData
def logInfo [MonadLog m] (stx : Syntax) (msgData : MessageData) : m Unit :=
log stx MessageSeverity.information msgData
def throwError {α} [MonadPosInfo m] [MonadExceptCore Exception m] (ref : Syntax) (msgData : MessageData) : m α := do
def throwError {α} [MonadPosInfo m] [MonadExcept Exception m] (ref : Syntax) (msgData : MessageData) : m α := do
msg ← mkMessage msgData MessageSeverity.error ref; throw (Exception.error msg)
def throwErrorUsingCmdPos {α} [MonadPosInfo m] [MonadExceptCore Exception m] (msgData : MessageData) : m α := do
def throwErrorUsingCmdPos {α} [MonadPosInfo m] [MonadExcept Exception m] (msgData : MessageData) : m α := do
cmdPos ← getCmdPos;
msg ← mkMessageAt msgData MessageSeverity.error cmdPos;
throw (Exception.error msg)