diff options
| author | Pierre Roux | 2020-09-03 13:12:00 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-11-04 20:53:47 +0100 |
| commit | 11a8997dd8fa83537607272692a3baf10dab342a (patch) | |
| tree | 2b88f003ab19f264d94f29806c28b48258800d28 /doc/tools/docgram/common.edit_mlg | |
| parent | dfcb15141a19db4f1cc61c14d1cdad0275009356 (diff) | |
[numeral notation] Adding the via ... using ... option
This enables numeral notations for non inductive types by
pre/postprocessing them to a given proxy inductive type.
For instance, this should enable the use of numeral notations for R.
Diffstat (limited to 'doc/tools/docgram/common.edit_mlg')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 5d0f9208fc..4d615a130a 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1285,10 +1285,10 @@ command: [ | WITH "Declare" "Scope" scope_name (* odd that these are in command while other notation-related ones are in syntax *) -| REPLACE "Numeral" "Notation" reference reference reference ":" ident number_modifier -| WITH "Numeral" "Notation" reference reference reference ":" scope_name number_modifier -| REPLACE "Number" "Notation" reference reference reference ":" ident number_modifier -| WITH "Number" "Notation" reference reference reference ":" scope_name number_modifier +| REPLACE "Number" "Notation" reference OPT number_via reference reference ":" ident number_modifier +| WITH "Number" "Notation" reference OPT number_via reference reference ":" scope_name number_modifier +| REPLACE "Numeral" "Notation" reference OPT number_via reference reference ":" ident number_modifier +| WITH "Numeral" "Notation" reference OPT number_via reference reference ":" scope_name number_modifier | REPLACE "String" "Notation" reference reference reference ":" ident | WITH "String" "Notation" reference reference reference ":" scope_name |