diff options
Diffstat (limited to 'doc/sphinx/user-extensions/proof-schemes.rst')
| -rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index e12e4d897a..682553c31b 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -26,6 +26,7 @@ induction for objects in type `identᵢ`. natural in case of inductively defined relations. .. cmdv:: Scheme Equality for @ident + :name: Scheme Equality Tries to generate a Boolean equality and a proof of the decidability of the usual equality. If `ident` involves some other inductive types, their equality has to be defined first. |