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

chore: remove workaround

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-27 13:15:31 -08:00
parent 89298b165d
commit 5981553e11
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/Meta/Basic.lean
View file

@ -141,7 +141,7 @@ instance : AddMessageContext MetaM := {
pure (a, sCore, s)
instance [MetaEval α] : MetaEval (MetaM α) :=
⟨fun env opts x _ => MetaEval.eval env opts (x.run' : CoreM _) true⟩ -- TODO: check why we need type ascription here
⟨fun env opts x _ => MetaEval.eval env opts x.run' true⟩
protected def throwIsDefEqStuck {α} : MetaM α :=
throw $ Exception.internal isDefEqStuckExceptionId