diff options
Diffstat (limited to 'doc/tools/coqrst/notations/TacticNotations.g')
| -rw-r--r-- | doc/tools/coqrst/notations/TacticNotations.g | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g new file mode 100644 index 00000000..a889ebda --- /dev/null +++ b/doc/tools/coqrst/notations/TacticNotations.g @@ -0,0 +1,33 @@ +/************************************************************************/ +/* * The Coq Proof Assistant / The Coq Development Team */ +/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */ +/* <O___,, * (see CREDITS file for the list of authors) */ +/* \VV/ **************************************************************/ +/* // * This file is distributed under the terms of the */ +/* * GNU Lesser General Public License Version 2.1 */ +/* * (see LICENSE file for the text of the license) */ +/************************************************************************/ +grammar TacticNotations; + +// Terminals are not visited, so we add non-terminals for each terminal that +// needs rendering (in particular whitespace (kept in output) vs. WHITESPACE +// (discarded)). + +top: blocks EOF; +blocks: block ((whitespace)? block)*; +block: atomic | meta | hole | repeat | curlies; +repeat: LGROUP (ATOM)? WHITESPACE blocks (WHITESPACE)? RBRACE; +curlies: LBRACE (whitespace)? blocks (whitespace)? RBRACE; +whitespace: WHITESPACE; +meta: METACHAR; +atomic: ATOM (SUB)?; +hole: ID (SUB)?; + +LGROUP: '{' [+*?]; +LBRACE: '{'; +RBRACE: '}'; +METACHAR: '%' [|(){}]; +ATOM: '@' | '_' | ~[@_{} ]+; +ID: '@' ('_'? [a-zA-Z0-9])+; +SUB: '_' '_' [a-zA-Z0-9]+; +WHITESPACE: ' '+; |