lean4-htt/src/Lean/Compiler/LCNF
2022-08-28 08:55:35 -07:00
..
Basic.lean fix: Compiler/LCNF/ElimDead.lean 2022-08-28 08:55:35 -07:00
Bind.lean feat: add FunDecl.etaExpand 2022-08-27 10:41:54 -07:00
Check.lean feat: check whether join points are fully applied at Check.lean 2022-08-25 18:17:54 -07:00
CompilerM.lean feat: modify FVarSubst used in the new code generator 2022-08-28 08:55:35 -07:00
CSE.lean feat: modify FVarSubst used in the new code generator 2022-08-28 08:55:35 -07:00
DependsOn.lean feat: new PullLetDecls.lean 2022-08-25 13:39:15 -07:00
ElimDead.lean fix: Compiler/LCNF/ElimDead.lean 2022-08-28 08:55:35 -07:00
InferType.lean feat: add FunDecl.etaExpand 2022-08-27 10:41:54 -07:00
JoinPoints.lean refactor: new LCNF frontend 2022-08-24 11:40:37 -07:00
LCtx.lean perf: improve FVarSubst apply functions in the new compiler stack 2022-08-26 20:10:36 -07:00
Main.lean chore: print decl size at trace message 2022-08-25 18:11:49 -07:00
PrettyPrinter.lean refactor: new LCNF frontend 2022-08-24 11:40:37 -07:00
PullLetDecls.lean chore: remove workarounds 2022-08-27 10:56:15 -07:00
PullLocalDecls.lean refactor: new LCNF frontend 2022-08-24 11:40:37 -07:00
Simp.lean feat: start simp for new LCNF format 2022-08-27 19:59:31 -07:00
Stage1.lean refactor: new LCNF frontend 2022-08-24 11:40:37 -07:00
ToDecl.lean fix: Core.transform API and uses 2022-08-25 19:07:42 -07:00
ToExpr.lean feat: new CSE.lean 2022-08-25 18:08:22 -07:00
ToLCNF.lean chore: remove workarounds 2022-08-27 10:56:15 -07:00
Types.lean feat: add FunDecl.etaExpand 2022-08-27 10:41:54 -07:00
Util.lean feat: att new LCNF/toLCNF.lean 2022-08-23 20:21:06 -07:00