diff options
| author | Clément Pit-Claudel | 2020-05-19 11:27:04 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-05-19 11:27:04 -0400 |
| commit | ed0f2f08e31ee4e645aa6e52970ddefc60f1f4f9 (patch) | |
| tree | 22277905fe446e6b0f47d5f9d7c1eb381c650128 /doc/sphinx/language | |
| parent | 5b23b80c8a0af603e8078616b2c5957a6f709e62 (diff) | |
| parent | c1125bda507137c35400808c6de19acfcece0ec7 (diff) | |
Merge PR #12224: Support :gdef:`text<term>` syntax (adding "<term>")
Reviewed-by: Zimmi48
Reviewed-by: cpitclaudel
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/core/basic.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/core/sorts.rst | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 250a0f0326..68900aa0be 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -267,7 +267,7 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types Intuitively, types may be viewed as sets containing terms. We say that a type is :gdef:`inhabited` if it contains at least one term (i.e. if we can find a term which is associated with this - type). We call such terms :gdef:`witness`\es. Note that deciding + type). We call such terms :gdef:`witnesses <witness>`. Note that deciding whether a type is inhabited is `undecidable <https://en.wikipedia.org/wiki/Undecidable_problem>`_. diff --git a/doc/sphinx/language/core/sorts.rst b/doc/sphinx/language/core/sorts.rst index 8307a02d6d..03581b95dd 100644 --- a/doc/sphinx/language/core/sorts.rst +++ b/doc/sphinx/language/core/sorts.rst @@ -22,7 +22,7 @@ Sorts | @universe_expr universe_expr ::= @universe_name {? + @num } -The types of types are called :gdef:`sort`\s. +The types of types are called :gdef:`sorts <sort>`. All sorts have a type and there is an infinite well-founded typing hierarchy of sorts whose base sorts are :math:`\SProp`, :math:`\Prop` |