From e6f3c19425a4f7280323c8815073f9a489b83652 Mon Sep 17 00:00:00 2001
From: joseville1001 <66519798+joseville1001@users.noreply.github.com>
Date: Sun, 14 Nov 2021 06:40:54 -0500
Subject: [PATCH] =?UTF-8?q?nit:=20Add=20caveat=20to=20rule=202.=20`=CE=BBx?=
 =?UTF-8?q?.c=20=3D=20Kc`=20(#4267)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

See this math stackexchange Q/A for the reason why this caveat is important: https://math.stackexchange.com/questions/4304294/rules-for-converting-lambda-calculus-expressions-to-ski-combinator-calculus-expr.

(There may be other clearer ways of wording the caveat. It is also not necessary that the caveat be shown inline with the rules; an alternative is to use a footnote or to make a note below the rules.)
---
 lambda-calculus.html.markdown | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lambda-calculus.html.markdown b/lambda-calculus.html.markdown
index 53a7a7cd..958dd746 100644
--- a/lambda-calculus.html.markdown
+++ b/lambda-calculus.html.markdown
@@ -131,7 +131,7 @@ We can convert an expression in the lambda calculus to an expression
 in the SKI combinator calculus:
 
 1. `λx.x = I`
-2. `λx.c = Kc`
+2. `λx.c = Kc` provided that `x` does not occur free in `c`
 3. `λx.(y z) = S (λx.y) (λx.z)`
 
 Take the church number 2 for example: