diff options
| author |  Anton Trunov <anton.a.trunov@gmail.com> | 2018-02-13 22:55:01 +0100 |
|---|---|---|
| committer | Anton Trunov <anton.a.trunov@gmail.com> | 2018-03-04 19:24:19 +0100 |
| commit | 5233abd2f876af6b9e5b705b2ab4df8cdb50b12e (patch) | |
| tree | dc071d2007b80eeaeb33b2b7b8b45fb70b197c8b /plugins/ssr | |
| parent | 78551857a41a57607ecfb3fd010e0a9755f47cea (diff) | |
ssr: fix typo in doc comment
Diffstat (limited to 'plugins/ssr')
| -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 f77f7c4fa..3aabff824 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -163,7 +163,7 @@ Require Import ssreflect. (* 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. *) (* Note that familiar "cancellation" identities like x + y - y = x or *) -(* x - y + x = x are respectively instances of right_loop and rev_right_loop *) +(* 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. *) (* *) (* - Morphisms for functions and relations: *) |