From 039007f93fa130261c97ec1188560777f1a297b9 Mon Sep 17 00:00:00 2001
From: Tanaka Akira
Date: Thu, 31 Jan 2019 16:18:07 +0900
Subject: Fix syntax of two lambda-abstractions.

In the note about η-reduction,
two lambda-abstraction used "," instead of ".".
---
 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 370ba2d87a..f8c223d4da 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -514,12 +514,12 @@ for :math:`x` an arbitrary variable name fresh in :math:`t`.
    then
 
    .. math::
-      λ x:\Type(1),(f~x) : ∀ x:\Type(1),\Type(1)
+      λ x:\Type(1).(f~x) : ∀ x:\Type(1),\Type(1)
    
    We could not allow
 
    .. math::
-      λ x:\Type(1),(f~x) \triangleright_η f
+      λ x:\Type(1).(f~x) \triangleright_η f
    
    because the type of the reduced term :math:`∀ x:\Type(2),\Type(1)` would not be
    convertible to the type of the original term :math:`∀ x:\Type(1),\Type(1).`
-- 
cgit v1.2.3