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

chore: fix confusing Environment.replayConsts parameter order (#7472)

Browse source
This commit is contained in:
Sebastian Ullrich 2025-03-13 13:35:45 +01:00 • committed by GitHub
parent a014ae1001
commit 0f3d426591
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Environment.lean
View file

@ -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