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/orderedGrammar | |
| 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/orderedGrammar')
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index a972ad4719..d12b3bf6cd 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -884,8 +884,8 @@ 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 number_modifier -| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT number_modifier +| "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 +910,7 @@ 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 qualid qualid ":" scope_name OPT number_modifier +| "Numeral" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT 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 ] @@ -1275,6 +1275,14 @@ number_modifier: [ | "(" "abstract" "after" bignat ")" ] +number_using: [ +| qualid qualid +] + +number_via: [ +| "via" qualid "using" "(" LIST1 number_using SEP "," ")" +] + hints_path: [ | "(" hints_path ")" | hints_path "*" |