source: src/common/CostLabel.ma @ 2768

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