source: src/common/PreIdentifiers.ma @ 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.

Also:

  • 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
Line 
1
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). *)
6
7include "basics/types.ma".
8include "ASM/String.ma".
9include "utilities/binary/positive.ma".
10
11(* identifiers and their generators are tagged to differentiate them, and to
12   provide extra type checking. *)
13
14inductive identifier (tag:String) : Type[0] ≝
15  an_identifier : Pos → identifier tag.
Note: See TracBrowser for help on using the repository browser.