max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Compiler
History
Cameron Zwarich 763a43c241
fix: correctly handle escaping functions in LCNF's elimDeadBranches pass (#8124) 
This PR correctly handles escaping functions in the LCNF
elimDeadBranches pass, by setting all params to top instead of
potentially leaving them at their default bottom value.
2025-04-26 23:56:01 +00:00
..
IR feat: LLVM 15 -> 19 (#6063) 2025-04-21 17:18:18 +00:00
LCNF fix: correctly handle escaping functions in LCNF's elimDeadBranches pass (#8124) 2025-04-26 23:56:01 +00:00
AtMostOnce.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
BorrowedAnnotation.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ClosedTermCache.lean fix: more realizeConst fixes (#7300) 2025-03-03 12:10:40 +00:00
ConstFolding.lean fix: constant folding for Nat.ble and Nat.blt (#6087) 2024-11-15 12:09:52 +00:00
CSimpAttr.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ExportAttr.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ExternAttr.lean feat: add support for extern LCNF decls (#6429) 2024-12-20 21:20:56 +00:00
FFI.lean chore: lake: bootstrap Lean include directory (#7967) 2025-04-15 23:15:53 +00:00
ImplementedByAttr.lean perf: Environment blocker removals from async-proofs branch (#7483) 2025-03-14 13:37:01 +00:00
InitAttr.lean chore: remove functions for compiling decls from Environment (#6600) 2025-01-13 18:51:06 +00:00
InlineAttrs.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
IR.lean chore: test that there are no orphaned modules (#8082) 2025-04-24 11:55:07 +00:00
LCNF.lean chore: test that there are no orphaned modules (#8082) 2025-04-24 11:55:07 +00:00
Main.lean feat: trace.profiler export to Firefox Profiler (#3801) 2024-04-15 12:13:14 +00:00
NameMangling.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
NeverExtractAttr.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
NoncomputableAttr.lean fix: perform an earlier 'noncomputable' check to avoid misoptimizations (#7824) 2025-04-06 16:01:07 +00:00
Old.lean perf: Environment blocker removals from async-proofs branch (#7483) 2025-03-14 13:37:01 +00:00
Options.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Specialize.lean fix: more realizeConst fixes (#7300) 2025-03-03 12:10:40 +00:00