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

feat: use Meta.Example.other ref : Syntax if it contains position information

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-06 10:06:24 -07:00
parent b1023872b3
commit 1eff4be172
1 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/Elab/Term.lean
View file

@ -236,7 +236,14 @@ mkMessageCore ctx.fileName ctx.fileMap msgData severity (ref.getPos.getD ctx.cmd
/-- Auxiliary function for `liftMetaM` -/
private def fromMetaException (ctx : Context) (ref : Syntax) (ex : Meta.Exception) : Exception :=
Exception.ex $ Elab.Exception.error $ mkMessageAux ctx ref ex.toMessageData MessageSeverity.error
let mk (ref : Syntax) : Exception :=
Exception.ex $ Elab.Exception.error $ mkMessageAux ctx ref ex.toMessageData MessageSeverity.error;
match ex with
| Meta.Exception.other ref' ex =>
match ref'.getPos with
| some _ => mk ref'
| _ => mk ref
| _ => mk ref
/-- Auxiliary function for `liftMetaM` -/
private def fromMetaState (ref : Syntax) (ctx : Context) (s : State) (newS : Meta.State) (oldTraceState : TraceState) : State :=