source: src/common/ @ 1873

Last change on this file since 1873 was 1515, checked in by campbell, 10 years ago

Add type of maps on positive binary numbers, and use them for identifers.


  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File size: 582 bytes
2(* Basic identifier definition.  This is done separately from the rest of the
3   definitions for identifiers so that error messages can use identifiers
4   and the other definitions can use the error monad (without having to
5   parametrise the monad by the type of error messages). *)
7include "basics/".
8include "ASM/".
9include "utilities/binary/".
11(* identifiers and their generators are tagged to differentiate them, and to
12   provide extra type checking. *)
14inductive identifier (tag:String) : Type[0] ≝
15  an_identifier : Pos → identifier tag.
Note: See TracBrowser for help on using the repository browser.