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

chore(library/init/lean/parser/parser): remove unnecessary import

Browse source 
It turns out we don't need evalConst for implementing `builtinParsers`.
This commit is contained in:
Leonardo de Moura 2019-06-19 10:53:51 -07:00
parent 5ccbb1ec1c
commit 401de35b6c
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
library/init/lean/parser/parser.lean
View file

@ -9,7 +9,6 @@ import init.lean.syntax
import init.lean.toexpr
import init.lean.environment
import init.lean.attributes
import init.lean.evalconst
import init.lean.parser.trie
import init.lean.parser.identifier
import init.lean.compiler.initattr