Changeset 2645 for src/joint/String.ma

Timestamp:

Feb 7, 2013, 9:22:22 PM (8 years ago)

Author:

sacerdot

Message:

1. some broken back-end files repaires, several still to go
2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files

File:

• src/joint/String.ma (moved) (moved from src/ASM/String.ma) (1 diff)

src/joint/String.ma

@@ -1 @@
-include "basics/lists/list.ma".
+include "basics/pts.ma".
 
-include "ASM/Char.ma".
-
-definition String ≝ list Char.
+(* Stupid definition, just to avoid an axiom in the extracted code *)
+(* Strings at the moment are only used in comments in the back-end *)
+axiom String: Type[0] ≝
+   EmptyString : String.