| .. |
|
Simp
|
fix: constant folding for UIntX (#10495)
|
2025-09-22 10:06:24 +00:00 |
|
AlphaEqv.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
AuxDeclCache.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
BaseTypes.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
Basic.lean
|
fix: do not allow access to private primitives in public scope (#9890)
|
2025-08-14 15:34:54 +00:00 |
|
Bind.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
Check.lean
|
chore: use ofConstName in error messages (#10121)
|
2025-08-25 23:20:36 +00:00 |
|
Closure.lean
|
perf: during specialization, don't abstract all local fun decls under binders (#9596)
|
2025-07-28 17:36:43 +00:00 |
|
CompatibleTypes.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
CompilerM.lean
|
fix: erase dependencies on let-bound fvars in internalizeCode (#9922)
|
2025-08-15 01:52:47 +00:00 |
|
ConfigOptions.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
CSE.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
DeclHash.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
DependsOn.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
ElimDead.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
ElimDeadBranches.lean
|
fix: correctly handle non-Nat literal types in LCNF elimDeadBranches (#9703)
|
2025-08-05 02:14:07 +00:00 |
|
ExtractClosed.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
FixedParams.lean
|
chore: don't check type of erased arguments in FixedParams analysis (#9602)
|
2025-08-05 02:41:36 +00:00 |
|
FloatLetIn.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
FVarUtil.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
InferType.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
Internalize.lean
|
fix: erase dependencies on let-bound fvars in internalizeCode (#9922)
|
2025-08-15 01:52:47 +00:00 |
|
JoinPoints.lean
|
chore: make Compiler.findJoinPoints trace messages more useful (#9668)
|
2025-08-01 17:42:32 +00:00 |
|
LambdaLifting.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
LCtx.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
Level.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
Main.lean
|
fix: inline/specialize may only refer to publicly imported decls for now (#10494)
|
2025-09-23 09:58:14 +00:00 |
|
MonadScope.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
MonoTypes.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
OtherDecl.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
Passes.lean
|
fix: inline/specialize may only refer to publicly imported decls for now (#10494)
|
2025-09-23 09:58:14 +00:00 |
|
PassManager.lean
|
refactor: split the LCNF pass list into separate base/mono lists (#9816)
|
2025-08-10 04:23:19 +00:00 |
|
PhaseExt.lean
|
chore: remove support for unused arity specification in ExternAttrData (#9552)
|
2025-07-25 21:23:56 +00:00 |
|
PrettyPrinter.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
Probing.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
PullFunDecls.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
PullLetDecls.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
ReduceArity.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
ReduceJpArity.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
Renaming.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
ScopeM.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
Simp.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
Specialize.lean
|
perf: inline dependent instances into specialized decls (#10080)
|
2025-08-24 00:12:27 +00:00 |
|
SpecInfo.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
StructProjCases.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
Testing.lean
|
refactor: split the LCNF pass list into separate base/mono lists (#9816)
|
2025-08-10 04:23:19 +00:00 |
|
ToDecl.lean
|
chore: use ofConstName in error messages (#10121)
|
2025-08-25 23:20:36 +00:00 |
|
ToExpr.lean
|
fix: overeager specialisation reuse in codegen (#10429)
|
2025-09-17 17:35:40 +00:00 |
|
ToLCNF.lean
|
chore: kernel changes ahead of String redefinition (#10330)
|
2025-09-17 09:12:07 +00:00 |
|
ToMono.lean
|
fix: incorporate info from _redArg decls for noncomputable check (#10040)
|
2025-08-22 01:02:40 +00:00 |
|
Types.lean
|
fix: check that compiler does not infer inconsistent types between modules (#10418)
|
2025-09-19 12:36:47 +00:00 |
|
Util.lean
|
refactor: module-ize Lean (#9330)
|
2025-07-25 12:02:51 +00:00 |
|
Visibility.lean
|
chore: overhaul meta error messages (#10569)
|
2025-09-26 12:56:46 +00:00 |
