diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-10-29 15:13:25 +0100 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:10 +0100 |
| commit | e13fed125d22e58e39487a3aa227416e1f2ba329 (patch) | |
| tree | c291ea3709d3dc158b04b33644e23f1e2bcb8259 /doc/refman/RefMan-cic.tex | |
| parent | 678f41f598f38c9c0ef7c587f7b876437a6d06d8 (diff) | |
COMMENT: question
Diffstat (limited to 'doc/refman/RefMan-cic.tex')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 56e9a2779..22cec45cc 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -313,6 +313,10 @@ be derived from the following rules. \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. +% QUESTION: At the moment, enrichment of a local context is denoted with ∷ +% whereas enrichment of the global environment is denoted with ; +% Is it necessary to use two different notations? +% Couldn't we use ∷ also for enrichment of the global context? \item[Ax] \index{Typing rules!Ax} \inference{\frac{\WFE{\Gamma}}{\WTEG{\Prop}{\Type(1)}}~~~~~ \frac{\WFE{\Gamma}}{\WTEG{\Set}{\Type(1)}}} |