3 commits

Author	SHA1	Message	Date
Leonardo de Moura	4a2fb6e922	chore: fix typo (#4929)	2024-08-06 15:27:20 +00:00
Leonardo de Moura	8e476e9d22	perf: instantiateExprMVars (#4915) ... TODO: - Support for `zeta := true` at `apply_beta`. - Investigate test failure. - Break PR in pieces because of bootstrapping issues. The current PR updates a stage0 file to workaround the issue. Motivation: significant performance improvement at https://github.com/leanprover/LNSym/blob/proof_size_expt/Proofs/SHA512/Experiments/Sym30.lean With M1 Pro: - Before: 4.56 secs - After: 3.16 secs Successfully built stage2 using this PR	2024-08-05 17:15:22 +00:00
Leonardo de Moura	1e9d96be22	perf: add lean_instantiate_level_mvars (#4910) ... The new code is not active yet because of bootstrapping issues. It requires an `update_stage0`.	2024-08-04 18:31:44 +00:00