|
Last change
on this file was
2394,
checked in by campbell, 7 years ago
|
|
I've kept the odd note on bits of CerCo? work I've been doing. James suggested
that it might be useful if these were recorded in the repository just in case
they contain some useful information that doesn't get recorded elsewhere.
|
|
File size:
372 bytes
|
| Line | |
|---|
| 1 | Current point: |
|---|
| 2 | |
|---|
| 3 | - Need to show fn_env_has for a register from choose_reg for the recursive call |
|---|
| 4 | to add_expr for unary ops, then that it is preserved over other changes to |
|---|
| 5 | the function being constructed. The current invariant, "fn_graph_included … |
|---|
| 6 | f f'" is not sufficient because it says nothing about the preservation of the |
|---|
| 7 | parameter and local register lists. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
