diff options
| author | Tanaka Akira | 2019-01-31 17:32:18 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-01-31 17:32:18 +0900 |
| commit | 000207cb082e016714ce21fd5e46baf281c41b9e (patch) | |
| tree | 38d6ecfd23f821006fae892b93dbb73b452d8f22 | |
| parent | 4af6783b8401e8165e3246be7c5460583788fe50 (diff) | |
Use \length for the function name of length.
| -rw-r--r-- | doc/sphinx/language/cic.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 153427dce6..44928c3683 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1205,7 +1205,7 @@ recursion (even terminating). So the basic idea is to restrict ourselves to primitive recursive functions and functionals. For instance, assuming a parameter :math:`A:\Set` exists in the local context, -we want to build a function length of type :math:`\List~A → \nat` which computes +we want to build a function :math:`\length` of type :math:`\List~A → \nat` which computes the length of the list, such that :math:`(\length~(\Nil~A)) = \nO` and :math:`(\length~(\cons~A~a~l)) = (\nS~(\length~l))`. We want these equalities to be @@ -1231,7 +1231,7 @@ principles. For instance, in order to prove :math:`(\kw{has}\_\kw{length}~A~(\cons~A~a~l)~(\length~(\cons~A~a~l)))` -which given the conversion equalities satisfied by length is the same +which given the conversion equalities satisfied by :math:`\length` is the same as proving: |