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

feat: improve error message

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-25 09:59:32 -07:00
parent 96b987c366
commit 67f007fb51
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1653,7 +1653,7 @@ where
let p (u : Level) := u.any fun | Level.mvar m _ => s.contains m | _ => false
let lhs := exposeRelevantUniverses (← instantiateMVars ctx.lhs) p
let rhs := exposeRelevantUniverses (← instantiateMVars ctx.rhs) p
addMessageContext m!"stuck at solving universe constraints{indentD m!"{entry.lhs} =?= {entry.rhs}"}\nwhile trying to unify{indentExpr lhs}\nwith{indentExpr rhs}"
addMessageContext m!"stuck at solving universe constraints{indentD m!"{entry.lhs} =?= {entry.rhs}"}\nwhile trying to unify{indentD m!"{lhs} : {← inferType lhs}"}\nwith{indentD m!"{rhs} : {← inferType rhs}"}"
@[specialize] def withoutPostponingUniverseConstraints (x : TermElabM α) : TermElabM α := do
let postponed ← getResetPostponed