doc-src/ZF/logics-ZF.rao
author paulson
Wed, 03 Feb 1999 14:02:49 +0100
changeset 6173 2c0579e8e6fa
parent 6156 0d52e7cbff29
permissions -rw-r--r--
documented typecheck_tac, etc
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6156
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
     1
% This file was generated by 'rail' from 'logics-ZF.rai'
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
     2
\rail@i {1}{ datatype : ( 'datatype' | 'codatatype' ) datadecls; \par datadecls: ( '"' id arglist '"' '=' (constructor + '|') ) + 'and' ; constructor : name ( () | consargs ) ( () | ( '(' mixfix ')' ) ) ; consargs : '(' ('"' var ':' term '"' + ',') ')' ; }
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
     3
\rail@o {1}{
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
     4
\rail@begin{2}{datatype}
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
     5
\rail@bar
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
     6
\rail@term{datatype}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
     7
\rail@nextbar{1}
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
     8
\rail@term{codatatype}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
     9
\rail@endbar
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    10
\rail@nont{datadecls}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    11
\rail@end
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    12
\rail@begin{3}{datadecls}
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    13
\rail@plus
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    14
\rail@term{"}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    15
\rail@nont{id}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    16
\rail@nont{arglist}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    17
\rail@term{"}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    18
\rail@term{=}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    19
\rail@plus
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    20
\rail@nont{constructor}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    21
\rail@nextplus{1}
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    22
\rail@cterm{|}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    23
\rail@endplus
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    24
\rail@nextplus{2}
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    25
\rail@cterm{and}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    26
\rail@endplus
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    27
\rail@end
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    28
\rail@begin{2}{constructor}
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    29
\rail@nont{name}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    30
\rail@bar
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    31
\rail@nextbar{1}
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    32
\rail@nont{consargs}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    33
\rail@endbar
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    34
\rail@bar
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    35
\rail@nextbar{1}
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    36
\rail@term{(}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    37
\rail@nont{mixfix}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    38
\rail@term{)}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    39
\rail@endbar
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    40
\rail@end
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    41
\rail@begin{2}{consargs}
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    42
\rail@term{(}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    43
\rail@plus
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    44
\rail@term{"}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    45
\rail@nont{var}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    46
\rail@term{:}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    47
\rail@nont{term}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    48
\rail@term{"}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    49
\rail@nextplus{1}
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    50
\rail@cterm{,}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    51
\rail@endplus
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    52
\rail@term{)}[]
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    53
\rail@end
0d52e7cbff29 *** empty log message ***
wenzelm
parents:
diff changeset
    54
}