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

refactor: narrow Lean imports

Browse source
This commit is contained in:
tydeu 2021-10-18 18:01:31 -04:00
parent bfedab0f9b
commit ffd5bc0f69
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Lake/Attributes.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lean
import Lean.Attributes
open Lean
namespace Lake

2
Lake/LeanConfig.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lean
import Lean.Elab.Frontend
import Lake.Package
import Lake.Attributes