source: src/common/CostLabel.ma @ 2768

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