Kyle Miller ac600853c0 fix: let the congr tactic handle "under-applied" applications (#9225) ... This PR improves the `congr` tactic so that it can handle function applications with fewer arguments than the arity of the head function. This also fixes a bug where `congr` could not make progress with `Set`-valued functions in Mathlib, since `Set` was being unfolded and making such functions have an apparently higher arity. This addresses issue #2128 for the `congr` tactic, but not `simp` and others.		2025-07-08 11:48:08 +00:00
..
Control	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Data	fix: let the congr tactic handle "under-applied" applications (#9225)	2025-07-08 11:48:08 +00:00
Grind	perf: synthesize ToInt instances on demand (#9241)	2025-07-08 02:36:16 +00:00
GrindInstances	fix: refactor grind's module/ring design to avoid a diamond (#9168)	2025-07-03 06:50:46 +00:00
Internal	feat: eliminate letFun support, deprecate let_fun syntax (#9086)	2025-06-30 02:10:18 +00:00
Omega	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
System	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
BinderNameHint.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
BinderPredicates.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
ByCases.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Classical.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Coe.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Control.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Conv.lean	feat: eliminate letFun support, deprecate let_fun syntax (#9086)	2025-06-30 02:10:18 +00:00
Core.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Data.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Dynamic.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Ext.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
GetElem.lean	feat: pattern inference using symbol priorities in grind (#9182)	2025-07-03 16:47:38 -07:00
Grind.lean	feat: pattern inference using symbol priorities in grind (#9182)	2025-07-03 16:47:38 -07:00
GrindInstances.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Guard.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Hints.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Internal.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
MacroTrace.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Meta.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
MetaTypes.lean	doc: use modern configuration syntax in the Simp.Config documentation (#9174)	2025-07-03 14:16:37 +00:00
Notation.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
NotationExtra.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Omega.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Prelude.lean	feat: Make Std.Do universe polymorphic (#9194)	2025-07-07 13:11:41 +00:00
PropLemmas.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
RCases.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
ShareCommon.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
SimpLemmas.lean	feat: eliminate letFun support, deprecate let_fun syntax (#9086)	2025-06-30 02:10:18 +00:00
Simproc.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
SizeOf.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
SizeOfLemmas.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Syntax.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
System.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Tactics.lean	feat: Make Std.Do universe polymorphic (#9194)	2025-07-07 13:11:41 +00:00
TacticsExtra.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Task.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Try.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Util.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
WF.lean	fix: module system: remove WellFounded-specific hacks (#9143)	2025-07-02 11:58:50 +00:00
WFTactics.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
While.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00