|
Last change
on this file since 2768 was
2767,
checked in by mckinna, 8 years ago
|
|
WARNING: BIG commit, which pushes code_size_opt check into LIN/LINToASM.ma
following CSC's comment on my previous partial commit
plus rolls all the miscellaneous code motion into the rest of the repo.
suggest REBUILD compiler.ma/correctness.ma from scratch.
|
|
File size:
299 bytes
|
| Rev | Line | |
|---|
| [2767] | 1 | include "common/Identifiers.ma". |
|---|
| [177] | 2 | |
|---|
| [738] | 3 | definition costlabel ≝ identifier CostTag. |
|---|
| [737] | 4 | |
|---|
| [2767] | 5 | definition costlabel_eq : ∀x,y:costlabel. (x=y) + (x≠y) ≝ identifier_eq ?. |
|---|
| 6 | |
|---|
| [737] | 7 | (* For use in importing programs in intermediate languages. *) |
|---|
| [747] | 8 | definition costlabel_of_nat : nat → costlabel ≝ identifier_of_nat ?. |
|---|
| [2703] | 9 | |
|---|
Note: See
TracBrowser
for help on using the repository browser.
