max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Compiler/IR
History
Leonardo de Moura 0684c95d35
fix: do not lift (<- ...) over pure if-then-else (#3820) 
Now, only `(<- ...)`s occurring in the condition of a pure if-then-else
are lifted.
That is, `if (<- foo) then ... else ...` is ok, but `if ... then (<-
foo) else ...` is not. See #3713

closes #3713 

This PR also adjusts this repo. Note that some of the `(<- ...)` were
harmless since they were just accessing some
read-only state.
2024-04-01 21:33:59 +00:00
..
Basic.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Borrow.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Boxing.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Checker.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
CompilerM.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
CtorLayout.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ElimDeadBranches.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ElimDeadVars.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
EmitC.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
EmitLLVM.lean fix: do not lift (<- ...) over pure if-then-else (#3820) 2024-04-01 21:33:59 +00:00
EmitUtil.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ExpandResetReuse.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Format.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
FreeVars.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
LiveVars.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
LLVMBindings.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
NormIds.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
PushProj.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
RC.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ResetReuse.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
SimpCase.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Sorry.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
UnboxResult.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00