diff options
| author | Timothy Bourke | 2018-07-22 10:56:23 +0200 |
|---|---|---|
| committer | Timothy Bourke | 2018-07-22 10:56:23 +0200 |
| commit | 80883ddf89949afa82081ba80ccb4934320e6ee3 (patch) | |
| tree | e24174e9c640df74eb75ecaf2a87e7bb4ff703a3 | |
| parent | f25c1d252ad61b4dc4321e3a11f33b1e6d4e3dff (diff) | |
Docs: minor typo in "Template Polymorphism"
| -rw-r--r-- | doc/sphinx/language/cic.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index b670305389..721dc80b18 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1019,7 +1019,7 @@ Template polymorphism +++++++++++++++++++++ Inductive types declared in :math:`\Type` are polymorphic over their arguments -in :math:`\Type`. If :math:`A` is an arity of some sort and math:`s` is a sort, we write :math:`A_{/s}` +in :math:`\Type`. If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}` for the arity obtained from :math:`A` by replacing its sort with :math:`s`. Especially, if :math:`A` is well-typed in some global environment and local context, then :math:`A_{/s}` is typable by typability of all products in the |