changed syntax diagrams according to quote-less consts and syntax section
authorclasohm
Wed, 29 Nov 1995 16:58:30 +0100
changeset 1373 f061d2435d63
parent 1372 16330e3fa3b7
child 1374 5e407f2a3323
changed syntax diagrams according to quote-less consts and syntax section
doc-src/Ref/theory-syntax.tex
--- a/doc-src/Ref/theory-syntax.tex	Wed Nov 29 16:56:54 1995 +0100
+++ b/doc-src/Ref/theory-syntax.tex	Wed Nov 29 16:58:30 1995 +0100
@@ -70,8 +70,23 @@
 consts : 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + )
        ;
 
-constDecl : ( name + ',') '::' string ;
+constDecl : ( name + ',') '::' (string | constType) ;
+
+constType : ( applParam * ) applLast;
+
+applParam : ( complexType | '(' paramType ')' |
+              '[' (paramType + ',') ']' ) '=>';
+
+applLast: ( simpleType | '(' (paramType + ',') ')' ) (id *);
 
+complexType: ( simpleType | '(' complexType ')' ) ( id + ) |
+             '(' ( ( complexType | '(' complexType ')' ) + ',' ) ')'
+             id +;
+
+paramType: ( complexType | '(' paramType ')' | '[' ( paramType + ',' ) ']' )
+           ( '=>' paramType * );
+
+simpleType: id | ( tid ( () | '::' id ) );
 
 mixfix :  string ( () | ( () | ('[' (nat + ',') ']')) nat )
        | infix