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

chore: move Std -> Bootstrap

Browse source
This commit is contained in:
Mario Carneiro 2022-08-29 01:03:08 -04:00
parent 1c5ec65260
commit f4bae4cd2a
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Lake/Util/DRBMap.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Mac Malone
-/
import Std.Data.RBMap
import Bootstrap.Data.RBMap
import Lake.Util.Compare
namespace Lake