From 5ef12ec1f5d6efa10ac450273d06c9eb9315b4ea Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sun, 8 Dec 2024 20:40:09 -0600 Subject: [PATCH] Update Load.lean --- DocGen4/Load.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index 74f4101..113bade 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -11,7 +11,7 @@ open Lean System IO def envOfImports (imports : Array Name) : IO Environment := do -- needed for modules which use syntax registered with `initialize add_parser_alias ..` - Lean.enableInitializersExecution + unsafe Lean.enableInitializersExecution importModules (imports.map (Import.mk ยท false)) Options.empty (leakEnv := true) def loadInit (imports : Array Name) : IO Hierarchy := do