diff options
| author | Tanaka Akira | 2019-01-31 19:24:39 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-01-31 19:24:39 +0900 |
| commit | 6f53aca07665c45af6c1713869f5434208607188 (patch) | |
| tree | c196798b31246a2b07578f38897f0c5f509e930b | |
| parent | fcb4cf7628ea67cf342f8c39cb7f5151897ff72c (diff) | |
The subst Γ{c}{(c c')} should be Γ{c'}{(c' c)}.
c can be non-function since c:U.
So, c c' is not typeable.
| -rw-r--r-- | doc/sphinx/language/cic.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index e3fd543c93..6ea3bcef23 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1766,12 +1766,12 @@ and :math:`\subst{E}{|Γ|}{|Γ|c}` to mean the parallel substitution .. math:: \frac{\WF{E;~c:U;~E′;~c′:=t:T;~E″}{Γ}} {\WF{E;~c:U;~E′;~c′:=λ x:U.~\subst{t}{c}{x}:∀x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}} - {\subst{Γ}{c}{(c~c′)}}} + {\subst{Γ}{c′}{(c′~c)}}} .. math:: \frac{\WF{E;~c:U;~E′;~c′:T;~E″}{Γ}} - {\WF{E;~c:U;~E′;~c′:∀ x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}}{\subst{Γ}{c}{(c~c′)}}} + {\WF{E;~c:U;~E′;~c′:∀ x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}}{\subst{Γ}{c′}{(c′~c)}}} .. math:: \frac{\WF{E;~c:U;~E′;~\ind{p}{Γ_I}{Γ_C};~E″}{Γ}} |