Spaces:
Running
Running
Update extract.lean
Browse files- extract.lean +1 -4
extract.lean
CHANGED
@@ -63,10 +63,7 @@ def main : IO Unit := do
|
|
63 |
IO.eprintln "\n\n"
|
64 |
IO.eprintln "importing modules"
|
65 |
searchPathRef.set compile_time_search_path%
|
66 |
-
CoreM.withImportModules #[`Mathlib]
|
67 |
-
-- (`maxHeartbeats, .ofNat 0),
|
68 |
-
(`smartUnfolding, .ofBool false),
|
69 |
-
]}) do
|
70 |
IO.eprintln s!"simplification timeout: {β getMaxHeartbeats}"
|
71 |
let env β getEnv
|
72 |
|
|
|
63 |
IO.eprintln "\n\n"
|
64 |
IO.eprintln "importing modules"
|
65 |
searchPathRef.set compile_time_search_path%
|
66 |
+
CoreM.withImportModules #[`Mathlib] do
|
|
|
|
|
|
|
67 |
IO.eprintln s!"simplification timeout: {β getMaxHeartbeats}"
|
68 |
let env β getEnv
|
69 |
|