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

fix: add Std to builtin path

Browse source
This commit is contained in:
Leonardo de Moura 2020-05-22 14:47:24 -07:00
parent dea832b63b
commit 1eaae47bab
2 changed files with 11 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Init/Lean/Util/Path.lean
View file

@ -49,8 +49,11 @@ appDir ← IO.appDir;
let installedLibDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "lib" ++ pathSep ++ "lean" ++ pathSep ++ "Init";
installedLibDirExists ← IO.isDir installedLibDir;
if installedLibDirExists then do
path ← realPathNormalized installedLibDir;
pure $ HashMap.empty.insert "Init" path
initPath ← realPathNormalized installedLibDir;
let map := HashMap.empty.insert "Init" initPath;
let stdDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "lib" ++ pathSep ++ "lean" ++ pathSep ++ "Std";
stdPath ← realPathNormalized stdDir;
pure $ map.insert "Std" stdPath
else
pure ∅

6
src/Std.lean Normal file
View file

@ -0,0 +1,6 @@
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Std.Data