# HG changeset patch # User clasohm # Date 817824009 -3600 # Node ID 63c3d78df538bfa50c31d8d2902e1f4f46374ed1 # Parent 007ad29ce6cacaaedbf7067fca549ca3ab2c8c84 changed typeDecl diff -r 007ad29ce6ca -r 63c3d78df538 doc-src/Ref/theory-syntax.tex --- a/doc-src/Ref/theory-syntax.tex Fri Dec 01 14:17:50 1995 +0100 +++ b/doc-src/Ref/theory-syntax.tex Fri Dec 01 14:20:09 1995 +0100 @@ -53,7 +53,14 @@ types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + ) ; -typeDecl : ( () | tid | '(' ( tid + ',' ) ')') name ( () | '=' string ); +typeDecl : ( () | tid | '(' ( tid + ',' ) ')') name + ( () | '=' ( string | type ) ); + +type : simpleType | '(' type ')' | type '=>' type | + '[' ( type + "," ) ']' '=>' type; + +simpleType: id | ( tid ( () | '::' id ) ) | + '(' ( type + "," ) ')' id | simpleType id; infix : ( 'infixr' | 'infixl' ) nat; @@ -72,12 +79,6 @@ constDecl : ( name + ',') '::' (string | type); -type : simpleType | '(' type ')' | type '=>' type | - '[' ( type + "," ) ']' '=>' type; - -simpleType: id | ( tid ( () | '::' id ) ) | - '(' ( type + "," ) ')' id | simpleType id; - mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) | infix | 'binder' string nat ;