lean4-htt/src/Lean/Compiler/LCNF
2025-09-08 05:52:45 +00:00
..
Simp chore: use ofConstName in error messages (#10121) 2025-08-25 23:20:36 +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 chore: add separate profiling entries for base, mono, and IR phases (#9817) 2025-08-10 05:00:49 +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 refactor: split the LCNF pass list into separate base/mono lists (#9816) 2025-08-10 04:23:19 +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 refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
ToLCNF.lean chore: use ofConstName in error messages (#10121) 2025-08-25 23:20:36 +00:00
ToMono.lean fix: incorporate info from _redArg decls for noncomputable check (#10040) 2025-08-22 01:02:40 +00:00
Types.lean chore: remove unnecessary parens (#10298) 2025-09-08 05:52:45 +00:00
Util.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Visibility.lean perf: do not cause compiler.small to export IR bodies unless the Expr body is already being exported (#10002) 2025-08-26 15:12:08 +00:00