diff options
| author | Antonio Nikishaev | 2019-10-13 20:44:04 +0400 |
|---|---|---|
| committer | Antonio Nikishaev | 2019-10-13 20:53:28 +0400 |
| commit | 7c0352e40af80c222507b1ddcf5e3a2ad29feb67 (patch) | |
| tree | a2cda3689604d5d17a7d07cd0a4f2756ecdf7c8e | |
| parent | 7f039cac07526881da1a149b8c0e49be32c2e89e (diff) | |
fix rev_right_loop doc
| -rw-r--r-- | plugins/ssr/ssrfun.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index 0ce3752a51..dc774e811e 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -166,7 +166,7 @@ Require Import ssreflect. right_loop inv op <-> op, inv obey the inverse loop right axiom: (x op y) op (inv y) = x for all x, y. rev_right_loop inv op <-> op, inv obey the inverse loop reverse right - axiom: (x op y) op (inv y) = x for all x, y. + axiom: (x op (inv y)) op y = x for all x, y. Note that familiar "cancellation" identities like x + y - y = x or x - y + y = x are respectively instances of right_loop and rev_right_loop The corresponding lemmas will use the K and NK/VK suffixes, respectively. |