The source files are grouped in planes
- according to the following table.
- Notation files covering the whole specification are provided.
- The notation for the relations or functions introduced in each file
- is shown in parentheses (? are placeholders).
+
Logical Structure of the Specification
+
+
This table reports the specification's components and their planes.
+ component |
plane |
files |
@@ -135,32 +198,26 @@
|
- natural numbers with infinity |
+ natural numbers with infinity |
+ |
ynat ( â ) |
ynat_pred ( â«°? ) |
ynat_succ ( ⫯? ) |
- ynat_le ( ?� ) |
- ynat_lt ( ?<? ) |
+ ynat_le ( ? ⤠? ) |
+ ynat_lt ( ? < ? ) |
ynat_minus ( ? - ? ) |
ynat_plus ( ? + ? ) |
ynat_max |
ynat_min |
- extensions to the library |
- arith.ma ( ?^? ) |
-
-
- |
-
-
- |
-
-
- |
-
-
- |
+ extensions to the library |
+ |
+ star |
+ lstar |
+ bool ( â» ) ( â ) |
+ arith ( ?^? ) |
+ list ( â ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) |
|
@@ -175,7 +232,8 @@
- generated logical decomposables |
+ generated logical decomposables |
+ |
xoa ( ââ ) ( â¨â¨ ) ( â§â§ ) |
xoa_props ( ⥠) ( ⤠) |
@@ -204,10 +262,6 @@
|
-
Physical Structure of the Specification
-
The source files are grouped in directories,
- one for each plane.
-
@@ -234,6 +288,6 @@
-
Last update: Mon, 15 Sep 2014 16:17:55 +0200
+
Last update: Tue, 04 Nov 2014 16:28:52 +0100