From 42bc6762952b2d4996e26285720b3e556a63c96d Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Mon, 2 Nov 2015 15:25:20 +0100
Subject: QUESTION: Cannot we simplify the presentation of "Ind" and "Constr"
 typing rules like this?

---
 doc/refman/RefMan-cic.tex | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index f4d107ed8a..2eb79ce842 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -716,12 +716,9 @@ contains an inductive declaration.
 
 \begin{description}
 \item[Ind]  \index{Typing rules!Ind}
-\inference{\frac{\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E}{(I_j:A_j) \in E}}
-\inference{\frac{\WFE{\Gamma}~~~~\NInd{}{\Gamma_I}{\Gamma_C} \in E}{\WTEG{I_j}{A_j}}}
+  \inference{\frac{\WFE{\Gamma}\hskip2em\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E\hskip2em(a:A)\in\Gamma_I}{\WTEG{a}{A}}}
 \item[Constr]  \index{Typing rules!Constr}
-
-\inference{\frac{\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E}{(c_i:C_i) \in E}}
-\inference{\frac{\WFE{\Gamma}~~~~\NInd{}{\Gamma_I}{\Gamma_C} \in E}{\WTEG{c_i}{C_i}}}
+  \inference{\frac{\WFE{\Gamma}\hskip2em\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E\hskip2em(c:C)\in\Gamma_C}{\WTEG{c}{C}}}
 \end{description}
 
 \paragraph{Example.}
-- 
cgit v1.2.3