From e6199666b0e0ff900cf29b2dcdd38798bb64769f Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Mon, 19 Jun 2017 20:11:58 +0100
Subject: [PATCH] changed unicode := to ascii

---
 src/Stlc.lagda | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/Stlc.lagda b/src/Stlc.lagda
index e8a31a52..bc4932e7 100644
--- a/src/Stlc.lagda
+++ b/src/Stlc.lagda
@@ -76,12 +76,12 @@ data value : Term → Set where
 ## Substitution
 
 \begin{code}
-_[_≔_] : Term → Id → Term → Term
-(varᵀ x) [ y ≔ P ] = if x === y then P else (varᵀ x)
-(λᵀ x ∷ A ⟶ N) [ y ≔ P ] =  λᵀ x ∷ A ⟶ (if x === y then N else (N [ y ≔ P ])) 
-(L ·ᵀ M) [ y ≔ P ] =  (L [ y ≔ P ]) ·ᵀ (M [ y ≔ P ])
-(trueᵀ) [ y ≔ P ] = trueᵀ
-(falseᵀ) [ y ≔ P ] = falseᵀ
-(ifᵀ L then M else N) [ y ≔ P ] = ifᵀ (L [ y ≔ P ]) then (M [ y ≔ P ]) else (N [ y ≔ P ])
+_[_:=_] : Term → Id → Term → Term
+(varᵀ x) [ y := P ] = if x === y then P else (varᵀ x)
+(λᵀ x ∷ A ⟶ N) [ y := P ] =  λᵀ x ∷ A ⟶ (if x === y then N else (N [ y := P ])) 
+(L ·ᵀ M) [ y := P ] =  (L [ y := P ]) ·ᵀ (M [ y := P ])
+(trueᵀ) [ y := P ] = trueᵀ
+(falseᵀ) [ y := P ] = falseᵀ
+(ifᵀ L then M else N) [ y := P ] = ifᵀ (L [ y := P ]) then (M [ y := P ]) else (N [ y := P ])
 \end{code}