From 000207cb082e016714ce21fd5e46baf281c41b9e Mon Sep 17 00:00:00 2001
From: Tanaka Akira
Date: Thu, 31 Jan 2019 17:32:18 +0900
Subject: Use \length for the function name of length.

---
 doc/sphinx/language/cic.rst | 4 ++--
 1 file 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:
 
 
-- 
cgit v1.2.3