v4.20.1-rc1
Pre-release
Pre-release
chore: revise environment constant addition details (#8610) * Move constant registration with elab env from `Lean.addDecl` to `Lean.Environment.addDeclCore` for compatibility * Make module system behavior independent of `Elab.async` value