diff options
Diffstat (limited to 'doc/sphinx/language/core/conversion.rst')
| -rw-r--r-- | doc/sphinx/language/core/conversion.rst | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/doc/sphinx/language/core/conversion.rst b/doc/sphinx/language/core/conversion.rst index 0f27b65107..6b031cfea3 100644 --- a/doc/sphinx/language/core/conversion.rst +++ b/doc/sphinx/language/core/conversion.rst @@ -5,8 +5,14 @@ Conversion rules In |Cic|, there is an internal reduction mechanism. In particular, it can decide if two programs are *intentionally* equal (one says -*convertible*). Convertibility is described in this section. +:term:`convertible`). Convertibility is described in this section. +α-conversion +~~~~~~~~~~~~ + +Two terms are :gdef:`α-convertible <alpha-convertible>` if they are syntactically +equal ignoring differences in the names of variables bound within the expression. +For example `forall x, x + 0 = x` is α-convertible with `forall y, y + 0 = y`. .. _beta-reduction: @@ -153,7 +159,7 @@ relation :math:`t` reduces to :math:`u` in the global environment 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 :gdef:`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 |