# HG changeset patch # User clasohm # Date 817821708 -3600 # Node ID 7e97232c11591d1ae0ed0f2657a1157aceb23466 # Parent 57777949b2f8895411ac11244ae0d00f95cb7d0f corrected diagrams for type and simpleType diff -r 57777949b2f8 -r 7e97232c1159 doc-src/Ref/theory-syntax.tex --- a/doc-src/Ref/theory-syntax.tex Fri Dec 01 13:03:34 1995 +0100 +++ b/doc-src/Ref/theory-syntax.tex Fri Dec 01 13:41:48 1995 +0100 @@ -70,13 +70,13 @@ consts : 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + ) ; -constDecl : ( name + ',') '::' (string | constType); +constDecl : ( name + ',') '::' (string | type); -constType : simpleType | '(' constType ')' | '[' ( constType + "," ) ']' - '=>' constType | constType '=>' constType; +type : simpleType | '(' type ')' | type '=>' type | + '[' ( type + "," ) ']' '=>' type; simpleType: id | ( tid ( () | '::' id ) ) | - '(' ( constType + "," ) ')' ( id + ',' ) | simpleType ( id + ',' ); + '(' ( type + "," ) ')' id | simpleType id; mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) | infix