Bare-bones documentation to pass the lint test

doc/sphinx/addendum/rewrite-rules.rst

@@ -0,0 +1,38 @@
+.. _rewrite_rules:
+
+User-defined rewrite rules
+==========================
+
+.. warning::
+
+   The status of rewrite rules is highly experimental.
+
+   In particular, conversion checking through bytecode or native code
+   compilation currently does not understand rewrite rules.
+
+
+Declaring symbols
+-----------------
+
+Rewrite rules operate on symbols, which are their own kind of constants.
+
+.. cmd:: {| Symbol | Symbols } {| {+ ( @assumpt ) } | @assumpt }
+   :name: Symbol; Symbols
+
+   Symbols are declared in the same way as axioms, using the keyword ``Symbol``.
+
+   .. coqtop:: all
+
+      Symbol pplus : nat -> nat -> nat.
+      Notation "a ++ b" := (pplus a b).
+
+Declaring rules
+---------------
+
+.. cmd:: Rewrite {| Rule | Rules } @ident := @rewrite_rule {* with @rewrite_rule }
+  :name: Rewrite; Rule; Rules
+
+   Rewrite rules are declared in blocks, which bear a name.
+
+  .. prodn::
+     rewrite_rule ::= @constr ==> @constr

doc/sphinx/language/core/index.rst

@@ -48,3 +48,4 @@ will have to check their output.
    primitive
    ../../addendum/universe-polymorphism
    ../../addendum/sprop
+   ../../addendum/rewrite-rules

doc/sphinx/proof-engine/vernacular-commands.rst

@@ -189,7 +189,7 @@ described elsewhere
 
       .. prodn::
          logical_kind ::= {| @thm_token | @assumption_token }
-         | {| Definition | Example | Context | Primitive }
+         | {| Definition | Example | Context | Primitive | Symbol }
          | {| Coercion | Instance | Scheme | Canonical | SubClass }
          | {| Field | Method }
 

doc/tools/docgram/common.edit_mlg

@@ -555,6 +555,9 @@ gallina: [
 | REPLACE thm_token ident_decl binders ":" lconstr LIST0 [ "with" ident_decl binders ":" lconstr ]
 | WITH thm_token ident_decl binders ":" type LIST0 [ "with" ident_decl binders ":" type ]
 | DELETE assumptions_token inline assum_list
+| DELETE "Symbols" assum_list
+| REPLACE "Symbol" assum_list
+| WITH [ "Symbol" | "Symbols" ] assum_list
 | REPLACE inductive_token LIST1 inductive_or_record_definition SEP "with"
 | WITH "Inductive" inductive_definition LIST0 ( "with" inductive_definition )
 |   "Inductive" record_definition LIST0 ( "with" record_definition )
@@ -578,6 +581,9 @@ gallina: [
 | DELETE "Scheme" "Boolean" "Equality" "for" smart_global
 | DELETE "Scheme" "Equality" "for" smart_global
 | "Scheme" OPT "Boolean" "Equality" "for" smart_global
+| DELETE "Rewrite" "Rules" identref ":=" LIST1 rewrite_rule SEP "with"
+| REPLACE "Rewrite" "Rule" identref ":=" LIST1 rewrite_rule SEP "with"
+| WITH "Rewrite" [ "Rule" | "Rules" ]  identref ":=" rewrite_rule LIST0 ( "with" rewrite_rule )
 ]
 
 SPLICE: [
@@ -1946,8 +1952,9 @@ logical_kind: [
 | DELETE "Example"
 | DELETE "Context"
 | DELETE "Primitive"
+| DELETE "Symbol"
 (* SubClass was deleted from def_token *)
-| [ "Definition" | "Example" | "Context" | "Primitive" ]
+| [ "Definition" | "Example" | "Context" | "Primitive" | "Symbol" ]
 | DELETE "Coercion"
 | DELETE "Instance"
 | DELETE "Scheme"

doc/tools/docgram/fullGrammar

@@ -797,6 +797,8 @@ gallina: [
 | assumption_token inline assum_list
 | assumptions_token inline assum_list
 | def_token ident_decl def_body
+| "Symbol" assum_list
+| "Symbols" assum_list
 | "Let" ident_decl def_body
 | finite_token inductive_or_record_definition
 | inductive_token LIST1 inductive_or_record_definition SEP "with"
@@ -814,6 +816,8 @@ gallina: [
 | "Universe" LIST1 identref
 | "Universes" LIST1 identref
 | "Constraint" LIST1 univ_constraint SEP ","
+| "Rewrite" "Rule" identref ":=" LIST1 rewrite_rule SEP "with"
+| "Rewrite" "Rules" identref ":=" LIST1 rewrite_rule SEP "with"
 ]
 
 register_token: [
@@ -961,6 +965,10 @@ cofix_definition: [
 | ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations
 ]
 
+rewrite_rule: [
+| OPT [ univ_decl "|-" ] lconstr "==>" lconstr
+]
+
 scheme: [
 | scheme_kind
 | identref ":=" scheme_kind
@@ -1379,6 +1387,7 @@ logical_kind: [
 | "Context"
 | extended_def_token
 | "Primitive"
+| "Symbol"
 ]
 
 extended_def_token: [

doc/tools/docgram/orderedGrammar

@@ -566,6 +566,10 @@ cofix_definition: [
 | ident_decl LIST0 binder OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations
 ]
 
+rewrite_rule: [
+| OPT [ univ_decl "|-" ] term "==>" term
+]
+
 scheme_kind: [
 | scheme_type "for" reference "Sort" sort_family
 ]
@@ -880,6 +884,7 @@ command: [
 | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ]
 | assumption_token OPT ( "Inline" OPT ( "(" natural ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ]
 | [ "Definition" | "Example" ] ident_decl def_body
+| [ "Symbol" | "Symbols" ] [ LIST1 ( "(" assumpt ")" ) | assumpt ]
 | "Let" ident_decl def_body
 | "Inductive" inductive_definition LIST0 ( "with" inductive_definition )
 | "Inductive" record_definition LIST0 ( "with" record_definition )
@@ -896,6 +901,7 @@ command: [
 | "Universe" LIST1 ident
 | "Universes" LIST1 ident
 | "Constraint" LIST1 univ_constraint SEP ","
+| "Rewrite" [ "Rule" | "Rules" ] ident ":=" rewrite_rule LIST0 ( "with" rewrite_rule )
 | "CoInductive" inductive_definition LIST0 ( "with" inductive_definition )
 | "CoInductive" record_definition LIST0 ( "with" record_definition )
 | "Variant" ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] ":=" OPT "|" LIST1 constructor SEP "|" OPT decl_notations
@@ -1025,7 +1031,7 @@ search_item: [
 
 logical_kind: [
 | [ thm_token | assumption_token ]
-| [ "Definition" | "Example" | "Context" | "Primitive" ]
+| [ "Definition" | "Example" | "Context" | "Primitive" | "Symbol" ]
 | [ "Coercion" | "Instance" | "Scheme" | "Canonical" | "SubClass" ]
 | [ "Field" | "Method" ]
 ]

test-suite/success/rewrule.v

@@ -169,4 +169,4 @@ Definition id'@{i} : Type@{i} -> Type@{u} := fun (t: Type@{i}) => t.
 Fail Definition U' : Type@{u} := id' Type@{u}.
 
 Require Import Coq.Logic.Hurkens.
-Definition f' : False := TypeNeqSmallType.paradox U eq_refl.
+Check TypeNeqSmallType.paradox U eq_refl : False.