diff options
| author | Pierre Roux | 2020-09-03 13:14:00 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-11-05 00:20:16 +0100 |
| commit | c217bbe80e18255ee3e67fa6266736529d80636d (patch) | |
| tree | 3730ea847ac2dc75b52d6a9217c099fc53105ca1 /doc/tools/docgram/orderedGrammar | |
| parent | 14f301450a356915d131e9f9326b3fa7234241a8 (diff) | |
[numeral notation] Document the via ... using ... option
Diffstat (limited to 'doc/tools/docgram/orderedGrammar')
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index d12b3bf6cd..3d1041e592 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 OPT number_via qualid qualid ":" scope_name OPT number_modifier -| "Numeral" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT number_modifier | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) | "Typeclasses" "Transparent" LIST1 qualid | "Typeclasses" "Opaque" LIST1 qualid @@ -910,7 +908,8 @@ command: [ | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family | "Declare" "Left" "Step" one_term | "Declare" "Right" "Step" one_term -| "Numeral" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT number_modifier +| "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 ":" scope_name | "SubClass" ident_decl def_body | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ] @@ -1270,17 +1269,20 @@ field_mod: [ | "completeness" one_term (* ring plugin *) ] -number_modifier: [ +deprecated_number_modifier: [ +| | "(" "warning" "after" bignat ")" | "(" "abstract" "after" bignat ")" ] -number_using: [ -| qualid qualid +number_modifier: [ +| "warning" "after" bignat +| "abstract" "after" bignat +| number_via ] number_via: [ -| "via" qualid "using" "(" LIST1 number_using SEP "," ")" +| "via" qualid "mapping" "[" LIST1 ( qualid "=>" qualid ) SEP "," "]" ] hints_path: [ |