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

fix: rename parameter of withImportModules to match doc string

Browse source
This commit is contained in:
David Renshaw 2023-09-11 11:20:42 -04:00 • committed by Sebastian Ullrich
parent 3e755dc0e1
commit ba416f2c1c
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Environment.lean
View file

@ -803,9 +803,9 @@ def importModules (imports : Array Import) (opts : Options) (trustLevel : UInt32
/--
Create environment object from imports and free compacted regions after calling `act`. No live references to the
environment object or imported objects may exist after `act` finishes. -/
unsafe def withImportModules {α : Type} (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0) (x : Environment → IO α) : IO α := do
unsafe def withImportModules {α : Type} (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0) (act : Environment → IO α) : IO α := do
let env ← importModules imports opts trustLevel
try x env finally env.freeRegions
try act env finally env.freeRegions
/--
Environment extension for tracking all `namespace` declared by users.