lean4-htt/src/Lean/Compiler/LCNF
2022-09-01 20:52:08 -07:00
..
Basic.lean feat: check whether LetDecl and FunDecl match their values in the LCNF local context 2022-09-01 07:05:07 -07:00
Bind.lean feat: add FunDecl.etaExpand 2022-08-27 10:41:54 -07:00
Check.lean feat: check LCNF parameters 2022-09-01 07:17:53 -07:00
CompilerM.lean feat: add simpValue? back 2022-09-01 20:52:08 -07:00
CSE.lean feat: new code inliner 2022-08-31 18:10:32 -07:00
DependsOn.lean feat: new PullLetDecls.lean 2022-08-25 13:39:15 -07:00
ElimDead.lean feat: LCNF.simp .let case 2022-08-29 09:52:16 -07:00
InferType.lean doc: explanations for LCNF. 2022-08-29 07:17:25 -07:00
JoinPoints.lean refactor: new LCNF frontend 2022-08-24 11:40:37 -07:00
LCtx.lean feat: LCNF local context dead variable checker 2022-08-31 21:07:21 -07:00
Main.lean chore: only check if compiler.check is set to true 2022-09-01 07:18:47 -07:00
Passes.lean feat: add simp compiler pass 2022-08-31 18:10:32 -07:00
PassManager.lean feat: basic pass manager 2022-08-31 16:28:07 -07:00
PrettyPrinter.lean refactor: new LCNF frontend 2022-08-24 11:40:37 -07:00
PullLetDecls.lean feat: add pure field to LetDecl, add helper functions for updating LCNF code 2022-08-28 08:55:35 -07:00
PullLocalDecls.lean refactor: new LCNF frontend 2022-08-24 11:40:37 -07:00
Simp.lean feat: add simpValue? back 2022-09-01 20:52:08 -07:00
Stage1.lean refactor: new LCNF frontend 2022-08-24 11:40:37 -07:00
ToDecl.lean fix: erase dead variables 2022-08-31 20:43:13 -07:00
ToExpr.lean feat: new CSE.lean 2022-08-25 18:08:22 -07:00
ToLCNF.lean feat: LCNF local context dead variable checker 2022-08-31 21:07:21 -07:00
Types.lean doc: explanations for LCNF. 2022-08-29 07:17:25 -07:00
Util.lean feat: att new LCNF/toLCNF.lean 2022-08-23 20:21:06 -07:00