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

chore: remove leftover comment

Browse source
This commit is contained in:
Leonardo de Moura 2022-10-20 08:35:47 -07:00
parent dd8bbe9367
commit dddf9e8a3f
1 changed files with 0 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -226,11 +226,6 @@ abbrev TermElab := Syntax → Option Expr → TermElabM Expr
/-
Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the
whole monad stack at every use site. May eventually be covered by `deriving`.
TODO: this trick does not work in the old/new code generators anymore.
TODO: figure out a way to instruct the compiler to optimize this code once,
and then lambda lift all methods once. Perhaps, we should do it whenever the
instance is marked as always_inline.
-/
@[always_inline]
instance : Monad TermElabM :=