From 3a25b967a944fe37e1ad54e54a904d90311ef381 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 12 Sep 2020 09:13:44 +0200 Subject: Renaming numnotoption into number_modifier --- doc/tools/docgram/orderedGrammar | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'doc/tools/docgram/orderedGrammar') diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 12a7bc684d..a972ad4719 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 numeral_modifier -| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier +| "Number" "Notation" qualid qualid qualid ":" scope_name OPT number_modifier +| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT number_modifier | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) | "Typeclasses" "Transparent" LIST1 qualid | "Typeclasses" "Opaque" LIST1 qualid @@ -910,6 +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 | "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 ] @@ -1269,7 +1270,7 @@ field_mod: [ | "completeness" one_term (* ring plugin *) ] -numeral_modifier: [ +number_modifier: [ | "(" "warning" "after" bignat ")" | "(" "abstract" "after" bignat ")" ] -- cgit v1.2.3 From 11a8997dd8fa83537607272692a3baf10dab342a Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:12:00 +0200 Subject: [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. --- doc/tools/docgram/orderedGrammar | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) (limited to 'doc/tools/docgram/orderedGrammar') 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 "*" -- cgit v1.2.3 From c217bbe80e18255ee3e67fa6266736529d80636d Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:14:00 +0200 Subject: [numeral notation] Document the via ... using ... option --- doc/tools/docgram/orderedGrammar | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) (limited to 'doc/tools/docgram/orderedGrammar') 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: [ -- cgit v1.2.3 From 0520decfdc94d52a2f8658b9cf6a730e6d333f8f Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:23:00 +0200 Subject: [numeral notation] Handle implicit arguments --- doc/tools/docgram/orderedGrammar | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/tools/docgram/orderedGrammar') diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 3d1041e592..13d8979208 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1282,7 +1282,7 @@ number_modifier: [ ] number_via: [ -| "via" qualid "mapping" "[" LIST1 ( qualid "=>" qualid ) SEP "," "]" +| "via" qualid "mapping" "[" LIST1 [ qualid "=>" qualid | "[" qualid "]" "=>" qualid ] SEP "," "]" ] hints_path: [ -- cgit v1.2.3 From b6214bd4d5d3003e9b60411a717e84277feead24 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:27:00 +0200 Subject: [string notation] Handle parameterized inductives and non inductives --- doc/tools/docgram/orderedGrammar | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'doc/tools/docgram/orderedGrammar') diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 13d8979208..151438bbbd 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -910,7 +910,7 @@ command: [ | "Declare" "Right" "Step" one_term | "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 +| "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 ] @@ -1278,10 +1278,10 @@ deprecated_number_modifier: [ number_modifier: [ | "warning" "after" bignat | "abstract" "after" bignat -| number_via +| number_string_via ] -number_via: [ +number_string_via: [ | "via" qualid "mapping" "[" LIST1 [ qualid "=>" qualid | "[" qualid "]" "=>" qualid ] SEP "," "]" ] -- cgit v1.2.3