source: src/utilities/IdentifierTools.ma @ 699

Last change on this file since 699 was 699, checked in by mulligan, 9 years ago

More or less finished formalisation of LIN.

File size: 376 bytes
Line 
1include "utilities/Compare.ma".
2include "utilities/BitVectorTrieSet.ma".
3include "common/AST.ma".
4
5axiom compare: Identifier → Identifier → Compare.
6definition IdentifierSet ≝ BitVectorTrieSet 8.
7axiom Universe: Type[0].
8axiom fresh_prefix: IdentifierSet → Identifier → Identifier.
9axiom new_universe: Identifier → Universe.
10axiom fresh: Universe → Identifier.
11
Note: See TracBrowser for help on using the repository browser.