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

chore: move NameMap into a separate file

Browse source
This commit is contained in:
Mario Carneiro 2022-09-14 05:13:34 -04:00
parent 024a298eb7
commit 032dc4bc8f
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/Config/Dependency.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
-/
import Lean.Data.Name
import Lean.Data.NameMap
namespace Lake
open Lean System

2
Lake/Util/Name.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lean.Data.Name
import Lean.Data.NameMap
import Lake.Util.Compare
open Lean