Kyle Miller 32894e7349 feat: remove irreducible from letFun (#9087) ... This PR removes the `irreducible` attribute from `letFun`, which is one step toward removing special `letFun` support; part of #9086. Removing the attribute seems to break some `module` tests in stage2.		2025-06-30 00:04:59 +00:00
..
Control	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Data	feat: BEq instances for ByteArray/FloatArray (#9075)	2025-06-29 11:12:48 +00:00
Grind	feat: OfSemiring.toQ unexpander (#9076)	2025-06-29 11:22:24 +00:00
GrindInstances	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Internal	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +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: make private the default in module (#9044)	2025-06-28 16:30:53 +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: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Grind.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00: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	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +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: remove irreducible from letFun (#9087)	2025-06-30 00:04:59 +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: make private the default in module (#9044)	2025-06-28 16:30:53 +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 private the default in module (#9044)	2025-06-28 16:30:53 +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	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +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