diff options
| author | Tanaka Akira | 2020-09-30 02:50:21 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2020-09-30 02:50:21 +0900 |
| commit | a497cab1da80c148b4c3c815f003e980699dd6d0 (patch) | |
| tree | c3710f0f964bec7f70daecd996940dba2d36d5d4 | |
| parent | 9995c44df32858624a84a5f87f14a4a24124f84e (diff) | |
Wf.v defines Fix_eq, not fix_eq.
A commit at 2003-03-13 changed the lemma name.
https://github.com/coq/coq/commit/cb1ae314411d78952062e5092804b85d981ad6e1
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 765373619f..485dfd964d 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -677,7 +677,7 @@ fixpoint equation can be proved. .. index:: single: Fix_F (term) - single: fix_eq (term) + single: Fix_eq (term) single: Fix_F_inv (term) single: Fix_F_eq (term) @@ -696,7 +696,7 @@ fixpoint equation can be proved. forall (x:A) (r:Acc x), F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)) = Fix_F x r. Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F x r = Fix_F x s. - Lemma fix_eq : forall x:A, Fix x = F x (fun (y:A) (p:R y x) => Fix y). + Lemma Fix_eq : forall x:A, Fix x = F x (fun (y:A) (p:R y x) => Fix y). End FixPoint. End Well_founded. |