Leonardo de Moura b01ca8ee23 feat: use expose_names in try? (#6967) ... This PR ensures `try?` can suggest tactics that need to reference inaccessible local names. Example: ```lean /-- info: Try these: • · expose_names; induction as, bs_1 using app.induct <;> grind [= app] • · expose_names; induction as, bs_1 using app.induct <;> grind only [app] -/ #guard_msgs (info) in example : app (app as bs) cs = app as (app bs cs) := by have bs := 20 -- shadows `bs` in the target try? ```		2025-02-06 05:44:25 +00:00
..
bench	test: identifier completion benchmark (#6796)	2025-01-27 19:31:32 +00:00
compiler
elabissues
ir
lean	feat: use expose_names in try? (#6967)	2025-02-06 05:44:25 +00:00
pkg
playground	feat: align take/drop/extract across List/Array/Vector (#6860)	2025-01-30 01:24:25 +00:00
plugin
simpperf
.gitignore
common.sh
lean-toolchain