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

chore: remove unnecessary inline

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-13 14:28:56 -08:00
parent 770e7fc350
commit 92316dff89
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/Init/Lean/Meta/Basic.lean
View file

@ -135,7 +135,7 @@ do ctx ← read;
s ← get;
throw (f {env := s.env, mctx := s.mctx, lctx := ctx.lctx })
@[inline] def throwBug {α} (b : Bug) : MetaM α :=
def throwBug {α} (b : Bug) : MetaM α :=
throwEx $ Exception.bug b
/-- Execute `x` only in debugging mode. -/