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

revised StlcProp up to start of Substitution

Browse source
This commit is contained in:
Philip Wadler 2017-07-04 18:38:18 +01:00
parent 31aece1144
commit a50ccd7315
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/StlcProp.lagda
View file

@ -231,8 +231,7 @@ example-free₁ : x ∈ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x)
example-free₁ = free-λ f≢x (free-·₂ free-var)
example-free₂ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x)
example-free₂ (free-λ f≢x (free-·₁ free-var)) = f≢x refl
example-free₂ (free-λ f≢x (free-·₂ ()))
example-free₂ (free-λ f≢f _) = f≢f refl
\end{code}
@ -244,7 +243,7 @@ postulate
example-free₃ : x ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x) · var f)
example-free₄ : f ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x) · var f)
example-free₅ : x ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] var f · var x)
example-free₆ : x ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] var f · var x)
example-free₆ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] var f · var x)
\end{code}
Although `_∈_` may apperar to be a low-level technical definition,