diff options
| author | Hugo Herbelin | 2015-10-22 16:52:53 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:07 +0100 |
| commit | e8d816c7c6278199bcc61111c6dd76012f84519e (patch) | |
| tree | 645e308406aa5f3bd6dd30c02470b5a6c242108f | |
| parent | da46d24c2645add913e187ebfc76590140ecd6ff (diff) | |
More consistency in the names of inference rules.
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 20 |
1 files changed, 9 insertions, 11 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index ac62abbe55..e5a83a0c4b 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -339,19 +339,17 @@ A term $t$ is well typed in a global environment $E$ iff there exists a local context $\Gamma$ and a term $T$ such that the judgment \WTEG{t}{T} can be derived from the following rules. \begin{description} -\item[W-E] \inference{\WF{[]}{[]}} -\item[W-S] % Ce n'est pas vrai : x peut apparaitre plusieurs fois dans Gamma -\inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~~x \not\in - \Gamma % \cup E - } - {\WFE{\Gamma::(x:T)}}~~~~~ - \frac{\WTEG{t}{T}~~~~x \not\in - \Gamma % \cup E +\item[W-Empty] \inference{\WF{[]}{}} +\item[W-Local-Assum] % Ce n'est pas vrai : x peut apparaitre plusieurs fois dans Gamma +\inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~~x \not\in \Gamma % \cup E + }{\WFE{\Gamma::(x:T)}}} +\item[W-Local-Def] +\inference{\frac{\WTEG{t}{T}~~~~x \not\in \Gamma % \cup E }{\WFE{\Gamma::(x:=t:T)}}} -\item[Def] \inference{\frac{\WTE{}{t}{T}~~~c \notin E} - {\WF{E;c:=t:T}{}}} - \item[Assum] \inference{\frac{\WTE{}{T}{s}~~~~s \in \Sort~~~~c \notin E} +\item[W-Global-Assum] \inference{\frac{\WTE{}{T}{s}~~~~s \in \Sort~~~~c \notin E} {\WF{E;c:T}{}}} +\item[W-Global-Def] \inference{\frac{\WTE{}{t}{T}~~~c \notin E} + {\WF{E;c:=t:T}{}}} \item[Ax] \index{Typing rules!Ax} \inference{\frac{\WFE{\Gamma}}{\WTEG{\Prop}{\Type(1)}}~~~~~ \frac{\WFE{\Gamma}}{\WTEG{\Set}{\Type(1)}}} |