lean4-htt/src/Lean/Compiler/IR
2021-06-02 07:05:42 -07:00
..
Basic.lean refactor: use Ordering inside of rbmap instead of lt. 2021-04-27 07:58:58 -07:00
Borrow.lean chore: mixHash => mixUSizeHash 2021-06-02 07:05:42 -07:00
Boxing.lean feat: add IR.DeclInfo 2021-01-26 12:41:07 -08:00
Checker.lean chore: remove when and «unless» 2021-03-20 18:52:18 -07:00
CompilerM.lean fix: do not evaluate code containing sorry 2021-01-26 15:01:53 -08:00
CtorLayout.lean chore: update structure, class, inductive 2020-11-27 15:09:30 -08:00
ElimDeadBranches.lean feat: add IR.DeclInfo 2021-01-26 12:41:07 -08:00
ElimDeadVars.lean feat: add IR.DeclInfo 2021-01-26 12:41:07 -08:00
EmitC.lean chore: make explicit user and internal panics 2021-03-04 07:37:33 -08:00
EmitUtil.lean feat: add IR.DeclInfo 2021-01-26 12:41:07 -08:00
ExpandResetReuse.lean feat: add IR.DeclInfo 2021-01-26 12:41:07 -08:00
Format.lean feat: add IR.DeclInfo 2021-01-26 12:41:07 -08:00
FreeVars.lean feat: add IR.DeclInfo 2021-01-26 12:41:07 -08:00
LiveVars.lean refactor: use Ordering inside of rbmap instead of lt. 2021-04-27 07:58:58 -07:00
NormIds.lean feat: add IR.DeclInfo 2021-01-26 12:41:07 -08:00
PushProj.lean feat: add IR.DeclInfo 2021-01-26 12:41:07 -08:00
RC.lean refactor: use Ordering inside of rbmap instead of lt. 2021-04-27 07:58:58 -07:00
ResetReuse.lean feat: add IR.DeclInfo 2021-01-26 12:41:07 -08:00
SimpCase.lean feat: add IR.DeclInfo 2021-01-26 12:41:07 -08:00
Sorry.lean fix: do not evaluate code containing sorry 2021-01-26 15:01:53 -08:00
UnboxResult.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00