diff options
| author | Tanaka Akira | 2019-01-31 16:18:07 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-01-31 16:18:07 +0900 |
| commit | 039007f93fa130261c97ec1188560777f1a297b9 (patch) | |
| tree | bc9f4c8ace46443564da2e1ae2a5fc5d032f5131 /doc | |
| parent | a5abe07d98b089808b2a98b4a90f7974eddc52c7 (diff) | |
Fix syntax of two lambda-abstractions.
In the note about η-reduction,
two lambda-abstraction used "," instead of ".".
Diffstat (limited to 'doc')
| -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 370ba2d87a..f8c223d4da 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -514,12 +514,12 @@ for :math:`x` an arbitrary variable name fresh in :math:`t`. then .. math:: - λ x:\Type(1),(f~x) : ∀ x:\Type(1),\Type(1) + λ x:\Type(1).(f~x) : ∀ x:\Type(1),\Type(1) We could not allow .. math:: - λ x:\Type(1),(f~x) \triangleright_η f + λ x:\Type(1).(f~x) \triangleright_η f because the type of the reduced term :math:`∀ x:\Type(2),\Type(1)` would not be convertible to the type of the original term :math:`∀ x:\Type(1),\Type(1).` |