diff options
| author | Jim Fehrle | 2020-11-16 20:24:09 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2020-11-18 12:14:48 -0800 |
| commit | 00003b625ed3d5f3f2d79cf38ca6ad08e634432e (patch) | |
| tree | efb7599f68adf68be2f6aea86970745ea3ca5341 /doc/sphinx/proofs | |
| parent | 04b25a7635e796ad05ef7db537883594a5144a56 (diff) | |
Use only nats for occs_nums rather than ints
Diffstat (limited to 'doc/sphinx/proofs')
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index f3f69a2fdc..31050cb107 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -320,7 +320,7 @@ Performing computations ref_or_pattern_occ ::= @reference {? at @occs_nums } | @one_term {? at @occs_nums } occs_nums ::= {+ {| @natural | @ident } } - | - {| @natural | @ident } {* @int_or_var } + | - {+ {| @natural | @ident } } int_or_var ::= @integer | @ident unfold_occ ::= @reference {? at @occs_nums } |