From ba416f2c1cf5f7fe20e6004aa8ba32a9f902bf8b Mon Sep 17 00:00:00 2001 From: David Renshaw Date: Mon, 11 Sep 2023 11:20:42 -0400 Subject: [PATCH] fix: rename parameter of withImportModules to match doc string --- src/Lean/Environment.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 9f4043ccd4..8cb4cad2b4 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -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.