michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

changed unicode := to ascii

Browse source
This commit is contained in:
wadler 2017-06-19 20:11:58 +01:00
parent 196c2f44ce
commit e6199666b0
1 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Stlc.lagda
View file

@ -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}