feat: import Mathlib explicitly

leanprover-community · Oct 6, 2021 · b8fef29 · b8fef29
1 parent 33b28ef
commit b8fef29
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathport.lean b/Mathport.lean
@@ -24,7 +24,7 @@ def mathport1 (config : Config) (path : Path) : IO Unit := do
     let ipath : Path ← resolveMod3 pcfg mod3
     { module := ipath.package ++ ipath.mod4 : Import }
 
-  if imports.isEmpty then imports := #[{ module := `Mathport : Import }]
+  if imports.isEmpty then imports := #[{ module := `Mathport : Import }, { module := `Mathlib : Import }]
 
   let opts := ({} : Options) |>.setNat `maxRecDepth 2000