|
Last change
on this file since 2989 was
2767,
checked in by mckinna, 7 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
|
| Line | |
|---|
| 1 | include "common/Identifiers.ma". |
|---|
| 2 | |
|---|
| 3 | definition costlabel ≝ identifier CostTag. |
|---|
| 4 | |
|---|
| 5 | definition costlabel_eq : ∀x,y:costlabel. (x=y) + (x≠y) ≝ identifier_eq ?. |
|---|
| 6 | |
|---|
| 7 | (* For use in importing programs in intermediate languages. *) |
|---|
| 8 | definition costlabel_of_nat : nat → costlabel ≝ identifier_of_nat ?. |
|---|
| 9 | |
|---|
Note: See
TracBrowser
for help on using the repository browser.
