Ignore:
Timestamp:
Apr 14, 2011, 5:54:37 PM (10 years ago)
Author:
mulligan
Message:

Work from today.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r738 r753  
    4040include "ASM/BitVectorTrie.ma".
    4141
    42 inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝ an_id_map : BitVectorTrie A 16 → identifier_map tag A.
     42inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝
     43  an_id_map : BitVectorTrie A 16 → identifier_map tag A.
     44 
     45 
    4346definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝
    4447  λtag,A. an_id_map tag A (Stub A 16).
Note: See TracChangeset for help on using the changeset viewer.