diff options
| author | Tanaka Akira | 2020-09-30 02:44:24 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2020-09-30 02:44:24 +0900 |
| commit | 9995c44df32858624a84a5f87f14a4a24124f84e (patch) | |
| tree | 5c52b3178417ddb1d42b055f1e1450c42698c410 /doc/sphinx/language | |
| parent | ff74bba7c4ef0c6f3e17944b015e05fc23bad1af (diff) | |
Type{i} should be Type(i).
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/cic.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 768c83150e..f1ed64e52a 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -274,7 +274,7 @@ following rules. .. inference:: Prod-Type \WTEG{T}{s} - s \in \{\SProp, \Type{i}\} + s \in \{\SProp, \Type(i)\} \WTE{\Gamma::(x:T)}{U}{\Type(i)} -------------------------------- \WTEG{∀ x:T,~U}{\Type(i)} |