doc-src/Ref/theory-syntax.tex
changeset 3215 9e097d5cc246
parent 3130 1ffe03f4c700
child 4317 7264fa2ff2ec
equal deleted inserted replaced
3214:409382c0cc88 3215:9e097d5cc246
    67      ;
    67      ;
    68 
    68 
    69 types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + )
    69 types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + )
    70       ;
    70       ;
    71 
    71 
    72 infix : ( 'infixr' | 'infixl' ) nat
    72 infix : ( 'infixr' | 'infixl' ) (() | string) nat
    73       ;
    73       ;
    74 
    74 
    75 typeDecl : typevarlist name
    75 typeDecl : typevarlist name
    76            ( () | '=' ( string | type ) );
    76            ( () | '=' ( string | type ) );
    77 
    77 
   102                 ;
   102                 ;
   103 
   103 
   104 constDecl : ( name + ',') '::' (string | type);
   104 constDecl : ( name + ',') '::' (string | type);
   105 
   105 
   106 mixfix :  string ( () | ( () | ('[' (nat + ',') ']')) nat )
   106 mixfix :  string ( () | ( () | ('[' (nat + ',') ']')) nat )
   107        | ( 'infixr' | 'infixl' ) (() | string) nat
   107        |  infix
   108        | 'binder' string nat ;
   108        | 'binder' string nat ;
   109 
   109 
   110 trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + )
   110 trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + )
   111       ;
   111       ;
   112 
   112