From 1825e095e1097ddd273edaf67508e33be4fb8d62 Mon Sep 17 00:00:00 2001 From: tydeu Date: Sun, 22 Aug 2021 03:51:44 -0400 Subject: [PATCH] refactore: rename `ModuleM` --- Lake/BuildModule.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Lake/BuildModule.lean b/Lake/BuildModule.lean index 5c378dc91e..096ee9b1f2 100644 --- a/Lake/BuildModule.lean +++ b/Lake/BuildModule.lean @@ -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