diff options
| author | coqbot-app[bot] | 2020-11-05 15:32:31 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-05 15:32:31 +0000 |
| commit | afc828b3e207dd39c59d1501d570a88b2012fd2c (patch) | |
| tree | f9af32a8b25439a9eb6c8407f99ad94f78a64fda /doc/tools/docgram/orderedGrammar | |
| parent | b95c38d3d28a59da7ff7474ece0cb42623497b7d (diff) | |
| parent | e6f7517be65e9f5d2127a86e2213eb717d37e43f (diff) | |
Merge PR #12218: Numeral notations for non inductive types
Reviewed-by: herbelin
Reviewed-by: JasonGross
Reviewed-by: jfehrle
Ack-by: Zimmi48
Diffstat (limited to 'doc/tools/docgram/orderedGrammar')
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 7d773e3a5b..75c0ca1453 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -884,8 +884,6 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier -| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) | "Typeclasses" "Transparent" LIST1 qualid | "Typeclasses" "Opaque" LIST1 qualid @@ -910,7 +908,9 @@ command: [ | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family | "Declare" "Left" "Step" one_term | "Declare" "Right" "Step" one_term -| "String" "Notation" qualid qualid qualid ":" scope_name +| "Number" "Notation" qualid qualid qualid OPT ( "(" LIST1 number_modifier SEP "," ")" ) ":" scope_name +| "Numeral" "Notation" qualid qualid qualid ":" scope_name deprecated_number_modifier +| "String" "Notation" qualid qualid qualid OPT ( "(" number_string_via ")" ) ":" scope_name | "SubClass" ident_decl def_body | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ] | assumption_token OPT ( "Inline" OPT ( "(" natural ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ] @@ -1269,11 +1269,22 @@ field_mod: [ | "completeness" one_term (* ring plugin *) ] -numeral_modifier: [ +deprecated_number_modifier: [ +| | "(" "warning" "after" bignat ")" | "(" "abstract" "after" bignat ")" ] +number_modifier: [ +| "warning" "after" bignat +| "abstract" "after" bignat +| number_string_via +] + +number_string_via: [ +| "via" qualid "mapping" "[" LIST1 [ qualid "=>" qualid | "[" qualid "]" "=>" qualid ] SEP "," "]" +] + hints_path: [ | "(" hints_path ")" | hints_path "*" |