commit: 7d0769a2743e19a4a4a4ab921ae088b24fb58f70

[log]
author: Leonardo de Moura <leomoura@amazon.com>

Thu Nov 21 18:10:57 2024 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Thu Nov 21 18:10:57 2024 -0800
tree: 1dd3a13b0b7bfbe05c4e82e1370f2157b56fc90e
parent: 72e952eadc6a171310f1d8e9d6e78acf98421494 [diff]

fix: `Context.setConfig` must update `metaConfig` and `indexConfig` fields

This PR fixes a bug at `Context.setConfig`. It was not propagating
the configuration to the redundant fields (cache) `metaConfig` and `indexConfig`.

src/Lean/Meta/Tactic/Simp/Types.lean[diff]

1 file changed

tree: 1dd3a13b0b7bfbe05c4e82e1370f2157b56fc90e

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean (documentation source: doc/make/index.md).