fix: term macro errors should be fatal

This commit is contained in:
Sebastian Ullrich 2022-01-04 11:14:57 +01:00
parent a000ee4249
commit 64971a1e3c
3 changed files with 6 additions and 1 deletions

View file

@ -1216,7 +1216,8 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone :
withNestedTraces do
let env ← getEnv
match (← liftMacroM (expandMacroImpl? env stx)) with
| some (decl, Except.ok stxNew) =>
| some (decl, stxNew?) =>
let stxNew ← liftMacroM <| liftExcept stxNew?
withInfoContext' (mkInfo := mkTermInfo decl (expectedType? := expectedType?) stx) <|
withMacroExpansion stx stxNew <|
withRef stxNew <|

View file

@ -0,0 +1,3 @@
macro "foo" : term => Lean.Macro.throwError "Test Error"
#check foo

View file

@ -0,0 +1 @@
macroError.lean:3:7-3:10: error: Test Error