doc-src/Logics/logics.rao
author wenzelm
Sun, 29 Nov 1998 13:16:47 +0100
changeset 5989 9670dae0143d
parent 5763 58ed0a78906d
child 6407 ec60d821f3f6
permissions -rw-r--r--
proof_general_trans (experimental);

% This file was generated by 'rail' from 'logics.rai'
\rail@i {1}{ typedef : 'typedef' ( () | '(' name ')') type '=' set witness; \par type : typevarlist name ( () | '(' infix ')' ); set : string; witness : () | '(' id ')'; }
\rail@o {1}{
\rail@begin{2}{typedef}
\rail@term{typedef}[]
\rail@bar
\rail@nextbar{1}
\rail@term{(}[]
\rail@nont{name}[]
\rail@term{)}[]
\rail@endbar
\rail@nont{type}[]
\rail@term{=}[]
\rail@nont{set}[]
\rail@nont{witness}[]
\rail@end
\rail@begin{2}{type}
\rail@nont{typevarlist}[]
\rail@nont{name}[]
\rail@bar
\rail@nextbar{1}
\rail@term{(}[]
\rail@nont{infix}[]
\rail@term{)}[]
\rail@endbar
\rail@end
\rail@begin{1}{set}
\rail@nont{string}[]
\rail@end
\rail@begin{2}{witness}
\rail@bar
\rail@nextbar{1}
\rail@term{(}[]
\rail@nont{id}[]
\rail@term{)}[]
\rail@endbar
\rail@end
}
\rail@i {2}{ record : 'record' typevarlist name '=' parent (field +); \par parent : ( () | type '+'); field : name '::' type; }
\rail@o {2}{
\rail@begin{2}{record}
\rail@term{record}[]
\rail@nont{typevarlist}[]
\rail@nont{name}[]
\rail@term{=}[]
\rail@nont{parent}[]
\rail@plus
\rail@nont{field}[]
\rail@nextplus{1}
\rail@endplus
\rail@end
\rail@begin{2}{parent}
\rail@bar
\rail@nextbar{1}
\rail@nont{type}[]
\rail@term{+}[]
\rail@endbar
\rail@end
\rail@begin{1}{field}
\rail@nont{name}[]
\rail@term{::}[]
\rail@nont{type}[]
\rail@end
}
\rail@i {3}{ datatype : 'datatype' typedecls; \par typedecls: ( newtype '=' (cons + '|') ) + 'and' ; newtype : typevarlist id ( () | '(' infix ')' ) ; cons : name (argtype *) ( () | ( '(' mixfix ')' ) ) ; argtype : id | tid | ('(' typevarlist id ')') ; }
\rail@o {3}{
\rail@begin{1}{datatype}
\rail@term{datatype}[]
\rail@nont{typedecls}[]
\rail@end
\rail@begin{3}{typedecls}
\rail@plus
\rail@nont{newtype}[]
\rail@term{=}[]
\rail@plus
\rail@nont{cons}[]
\rail@nextplus{1}
\rail@cterm{|}[]
\rail@endplus
\rail@nextplus{2}
\rail@cterm{and}[]
\rail@endplus
\rail@end
\rail@begin{2}{newtype}
\rail@nont{typevarlist}[]
\rail@nont{id}[]
\rail@bar
\rail@nextbar{1}
\rail@term{(}[]
\rail@nont{infix}[]
\rail@term{)}[]
\rail@endbar
\rail@end
\rail@begin{3}{cons}
\rail@nont{name}[]
\rail@bar
\rail@nextbar{1}
\rail@plus
\rail@nont{argtype}[]
\rail@nextplus{2}
\rail@endplus
\rail@endbar
\rail@bar
\rail@nextbar{1}
\rail@term{(}[]
\rail@nont{mixfix}[]
\rail@term{)}[]
\rail@endbar
\rail@end
\rail@begin{3}{argtype}
\rail@bar
\rail@nont{id}[]
\rail@nextbar{1}
\rail@nont{tid}[]
\rail@nextbar{2}
\rail@term{(}[]
\rail@nont{typevarlist}[]
\rail@nont{id}[]
\rail@term{)}[]
\rail@endbar
\rail@end
}