From 0f3d426591ebcb63f1c38a3074fb2a2ebbae447f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 13 Mar 2025 13:35:45 +0100 Subject: [PATCH] chore: fix confusing `Environment.replayConsts` parameter order (#7472) --- src/Lean/Environment.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 74e85650e5..a98dd9f075 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -1916,7 +1916,7 @@ but not `oldEnv` and the environment extension state for extensions defining `re `skipExisting` is true, constants that are already in `dest` are not added. If `newEnv` and `dest` are not derived from `oldEnv`, the result is undefined. -/ -def replayConsts (oldEnv newEnv : Environment) (dest : Environment) (skipExisting := false) : +def replayConsts (dest : Environment) (oldEnv newEnv : Environment) (skipExisting := false) : BaseIO Environment := do let numNewConsts := newEnv.asyncConsts.size - oldEnv.asyncConsts.size let consts := newEnv.asyncConsts.revList.take numNewConsts |>.reverse