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

refactore: rename ModuleM

Browse source
This commit is contained in:
tydeu 2021-08-22 03:51:44 -04:00
parent 332af4c262
commit 1825e095e1
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
Lake/BuildModule.lean
View file

@ -149,13 +149,13 @@ def recFetchModuleOleanTargetWithLocalImports [Monad m] [MonadLiftT BuildM m]
-- ## Definitions
abbrev ModuleM (α) :=
abbrev ModuleFetchM (α) :=
-- equivalent to `RBTopT (cmp := Name.quickCmp) Name ModuleTarget BuildM`.
-- phrased this way to use `NameMap`
EStateT (List Name) (NameMap α) BuildM
abbrev ModuleFetch (α) :=
RecFetch Name α (ModuleM α)
RecFetch Name α (ModuleFetchM α)
abbrev OleanTargetFetch := ModuleFetch OleanTarget
abbrev ModuleTargetFetch := ModuleFetch ModuleTarget