Kyle Miller 764386734c fix: improvements to change tactic (#6022) ... This PR makes the `change` tactic and conv tactic use the same elaboration strategy. It works uniformly for both the target and local hypotheses. Now `change` can assign metavariables, for example: ```lean example (x y z : Nat) : x + y = z := by change ?a = _ let w := ?a -- now `w : Nat := x + y` ```		2024-11-16 07:08:29 +00:00
..
bench	test: synthetic simp_arith benchmark (#6061)	2024-11-13 15:49:52 +00:00
compiler
elabissues
ir
lean	fix: improvements to change tactic (#6022)	2024-11-16 07:08:29 +00:00
pkg	fix: make sure monad lift coercion elaborator has no side effects (#6024)	2024-11-13 16:22:31 +00:00
playground	feat: rename Array.shrink to take, and relate to List.take (#5796)	2024-10-21 23:35:32 +00:00
plugin
simpperf
.gitignore
common.sh
lean-toolchain