commit: 96d15f5d485c333e716b30b22172e95c671bf909

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

Thu Mar 19 15:41:33 2026 -0400
committer: Leonardo de Moura <leomoura@amazon.com>

Thu Mar 19 15:41:33 2026 -0400
tree: 2f57c7be3c7c540903b40020992888d46cbfab1a
parent: 0a8121e6096a2a5960a909598c81bebbbaa5b257 [diff]

test: add dependent forall test for contextDependent cache

Exercises `simpForall'` with `withFreshTransientCache` — the body
`n + 2 = 2 + n` is simplified context-dependently inside the binder.
The binder type `Nat` hits persistent cache on second traversal.

tests/elab/sym_simp_cd.lean[diff]

1 file changed

tree: 2f57c7be3c7c540903b40020992888d46cbfab1a

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.