diff options
| -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 962d2a94e3..b56f0cc9e3 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1632,7 +1632,7 @@ should be an inductive definition. For doing this, the syntax of fixpoints is extended and becomes .. math:: - \Fix~f_i\{f_1/k_1 :A_1':=t_1' … f_n/k_n :A_n':=t_n'\} + \Fix~f_i\{f_1/k_1 :A_1:=t_1 … f_n/k_n :A_n:=t_n\} where :math:`k_i` are positive integers. Each :math:`k_i` represents the index of |