From 10f9c82c38c6eb01e64ab9a8fa233300568c18d4 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Mon, 2 Nov 2015 16:39:28 +0100
Subject: ENH: adding a definition of the concept "_ is an arity".

There already exists a definition of the following concept:

  "_ is an arity of sort _"

I was not 100% sure what the following concept (used later in the text) means:

  "_ is an arity"

so I added this (simple) definition in order to avoid possible confusion.
---
 doc/refman/RefMan-cic.tex | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index eaf400f263..deaa1047c8 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -773,6 +773,9 @@ to the sort $s$ or to a product $\forall~x:T,U$ with $U$ an arity
 of sort $s$. (For instance $A\ra \Set$ or $\forall~A:\Prop,A\ra
 \Prop$ are arities of sort respectively \Set\ and \Prop).
 \vskip.5em
+\noindent A type $T$ is an {\em arity} if there is a $s\in\Sort$
+such that $T$ is an arity of sort $s$.
+\vskip.5em
 \noindent A {\em type
   of constructor of $I$}\index{Type of constructor} is either a term
 $(I~t_1\ldots ~t_n)$ or $\fa x:T,C$ with $C$ recursively 
-- 
cgit v1.2.3