Changeset 737 for src/common


Ignore:
Timestamp:
Apr 4, 2011, 5:13:09 PM (9 years ago)
Author:
campbell
Message:

Use more abstract identifiers in Clight / RTLabs.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/CostLabel.ma

    r720 r737  
    11include "Clight/AST.ma".
    22
    3 definition costlabel ≝ ident.
     3axiom CostTag : String.
     4
     5definition costlabel ≝ Identifier CostTag.
     6
     7(* For use in importing programs in intermediate languages. *)
     8definition costlabel_of_nat : nat → costlabel ≝ identifier_of_nat ?.
  • src/common/Identifiers.ma

    r736 r737  
    3232qed.
    3333
    34 definition identifer_of_nat : ∀tag:String. nat → Identifier tag ≝
     34definition identifier_of_nat : ∀tag:String. nat → Identifier tag ≝
    3535  λtag,n. an_identifier tag (bitvector_of_nat ? n).
    3636
Note: See TracChangeset for help on using the changeset viewer.