diff options
Diffstat (limited to 'doc/tools/coqrst/notations/TacticNotations.g')
-rw-r--r-- | doc/tools/coqrst/notations/TacticNotations.g | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g new file mode 100644 index 000000000..72ae8eb6b --- /dev/null +++ b/doc/tools/coqrst/notations/TacticNotations.g @@ -0,0 +1,30 @@ +/************************************************************************/ +/* * 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 | hole | repeat | curlies; +repeat: LGROUP (ATOM)? WHITESPACE blocks (WHITESPACE)? RBRACE; +curlies: LBRACE (whitespace)? blocks (whitespace)? RBRACE; +whitespace: WHITESPACE; +atomic: ATOM; +hole: ID; + +LGROUP: '{' [+*?]; +LBRACE: '{'; +RBRACE: '}'; +ATOM: ~[@{} ]+; +ID: '@' [a-zA-Z0-9_]+; +WHITESPACE: ' '+; |