diff options
| author | Tanaka Akira | 2019-01-31 16:14:38 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-01-31 16:14:38 +0900 |
| commit | a5abe07d98b089808b2a98b4a90f7974eddc52c7 (patch) | |
| tree | a23724981a99a0396e78c68da6992bfae864353c | |
| parent | ddcd0afd740278b7b18999cd8ad4aa01c8b26d5f (diff) | |
Change {\Sort} to \Sort.
After #9435 (Use \mathcal instead of \cal), \Sort doesn't have
font changing effect.
So, {\Sort} is same as \Sort now and the former is changed to latter in
cic.rst.
| -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 05878a9f33..370ba2d87a 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -328,7 +328,7 @@ following rules. .. inference:: Prod-Prop \WTEG{T}{s} - s \in {\Sort} + s \in \Sort \WTE{\Gamma::(x:T)}{U}{\Prop} ----------------------------- \WTEG{\forall~x:T,U}{\Prop} @@ -1865,7 +1865,7 @@ in the sort :math:`\Set`, which is extended to a domain in any sort: .. inference:: ProdImp E[Γ] ⊢ T : s - s ∈ {\Sort} + s ∈ \Sort E[Γ::(x:T)] ⊢ U : \Set --------------------- E[Γ] ⊢ ∀ x:T,U : \Set |