Ignore:
Timestamp:
Nov 18, 2011, 1:03:14 PM (9 years ago)
Author:
campbell
Message:

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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/PreIdentifiers.ma

    r797 r1515  
    77include "basics/types.ma".
    88include "ASM/String.ma".
    9 include "ASM/Arithmetic.ma".
     9include "utilities/binary/positive.ma".
    1010
    1111(* identifiers and their generators are tagged to differentiate them, and to
     
    1313
    1414inductive identifier (tag:String) : Type[0] ≝
    15   an_identifier : Word → identifier tag.
     15  an_identifier : Pos → identifier tag.
Note: See TracChangeset for help on using the changeset viewer.