diff options
| author | Matej Kosik | 2015-10-29 15:02:04 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:10 +0100 |
| commit | 678f41f598f38c9c0ef7c587f7b876437a6d06d8 (patch) | |
| tree | 3a32a082937159dcc0d064cd0334c20c27514275 | |
| parent | 13ebbb8ab04036298d288b47a4664379173e6e3c (diff) | |
COMMENT: question
| -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 1804ebd9ce..56e9a27790 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -312,6 +312,7 @@ be derived from the following rules. {\WF{E;c:T}{}}} \item[W-Global-Def] \inference{\frac{\WTE{}{t}{T}~~~c \notin E} {\WF{E;c:=t:T}{}}} +% QUESTION: Why, in case of W-Local-Assum and W-Global-Assum we need s ∈ S hypothesis. \item[Ax] \index{Typing rules!Ax} \inference{\frac{\WFE{\Gamma}}{\WTEG{\Prop}{\Type(1)}}~~~~~ \frac{\WFE{\Gamma}}{\WTEG{\Set}{\Type(1)}}} |