diff options
| author | Sam Pablo Kuper | 2018-10-21 19:04:42 +0100 |
|---|---|---|
| committer | Sam Pablo Kuper | 2018-10-23 03:55:52 +0100 |
| commit | 3674fd87795903bc0d6b654e73dc4dd2afcd53b0 (patch) | |
| tree | e786464dac480049f6e3b443ae9ecfc01531ebf1 | |
| parent | 2d714ebc0ea9588b4346249a574d9eda63dd389d (diff) | |
Order Greek letters consistently w/rest of document
| -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 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 |