diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-11-03 11:39:54 +0100 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:12 +0100 |
| commit | f07348e606882ddb0d69029bde82be3106335f21 (patch) | |
| tree | 8a29273ceaac2a2eb2aa879bee44dbb766c19b62 /doc | |
| parent | 8b559623f8f2539836069a7352498a5e2c4784e6 (diff) | |
COMMENT: question
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index f7a6470f9..5df70a8e9 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -305,6 +305,7 @@ 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-Empty] \inference{\WF{[]}{}} +% QUESTION: Why in W-Local-Assum and W-Local-Def we do not need x ∉ E hypothesis? \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)}}} |