aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorThéo Zimmermann2018-10-23 16:54:18 +0200
committerThéo Zimmermann2018-10-23 16:54:18 +0200
commit724d908c2e2e81cf36fe09da5a054f49f534629b (patch)
tree8cf90b361b777084132f3aa4f8a42a55b79949a7
parentfc1f3ef3e963ca0446b225d71f3f1414f0d4405b (diff)
parent3674fd87795903bc0d6b654e73dc4dd2afcd53b0 (diff)
Merge PR #8798: Order Greek letters consistently w/rest of document
-rw-r--r--doc/sphinx/language/cic.rst4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 381f8bb661..835d6dcaa6 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -533,10 +533,10 @@ Convertibility
Let us write :math:`E[Γ] ⊢ t \triangleright u` for the contextual closure of the
relation :math:`t` reduces to :math:`u` in the global environment
:math:`E` and local context :math:`Γ` with one of the previous
-reductions β, ι, δ or ζ.
+reductions β, δ, ι or ζ.
We say that two terms :math:`t_1` and :math:`t_2` are
-*βιδζη-convertible*, or simply *convertible*, or *equivalent*, in the
+*βδιζη-convertible*, or simply *convertible*, or *equivalent*, in the
global environment :math:`E` and local context :math:`Γ` iff there
exist terms :math:`u_1` and :math:`u_2` such that :math:`E[Γ] ⊢ t_1 \triangleright
… \triangleright u_1` and :math:`E[Γ] ⊢ t_2 \triangleright … \triangleright u_2` and either :math:`u_1` and