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

minor fixes to Stlc

Browse source
This commit is contained in:
Philip Wadler 2017-07-17 16:06:36 +01:00
parent 0432804150
commit 3b62e81c06
2 changed files with 2426 additions and 2432 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4829
out/Stlc.md
View file

File diff suppressed because it is too large Load diff

29
src/Stlc.lagda
View file

@ -117,11 +117,11 @@ data Term : Set where
We use the following special characters We use the following special characters
⇒ U+21D2: RIGHTWARDS DOUBLE ARROW (\=>) ⇒ U+21D2: RIGHTWARDS DOUBLE ARROW (\=>)
` U+0060: GRAVE ACCENT ` U+0060: GRAVE ACCENT
λ U+03BB: GREEK SMALL LETTER LAMBDA (\Gl or \lambda) λ U+03BB: GREEK SMALL LETTER LAMBDA (\Gl or \lambda)
∶ U+2236: RATIO (\:) ∶ U+2236: RATIO (\:)
· U+00B7: MIDDLE DOT (\cdot) · U+00B7: MIDDLE DOT (\cdot)
Note that ∶ (U+2236 RATIO) is not the same as : (U+003A COLON). Note that ∶ (U+2236 RATIO) is not the same as : (U+003A COLON).
Colon is reserved in Agda for declaring types. Everywhere that we Colon is reserved in Agda for declaring types. Everywhere that we
@ -237,18 +237,15 @@ currying. This is made more convenient by declaring `_⇒_` to
associate to the right and `_·_` to associate to the left. associate to the right and `_·_` to associate to the left.
Thus, Thus,
> `(𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹` abbreviates `(𝔹 ⇒ 𝔹) ⇒ (𝔹 ⇒ 𝔹)`, * `(𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹` abbreviates `(𝔹 ⇒ 𝔹) ⇒ (𝔹 ⇒ 𝔹)`
* `two · not · true` abbreviates `(two · not) · true`.
and similarly,
> `two · not · true` abbreviates `(two · not) · true`.
We choose the binding strength for abstractions and conditionals We choose the binding strength for abstractions and conditionals
to be weaker than application. For instance, to be weaker than application. For instance,
> `` λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x) `` abbreviates * `` λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x) `` abbreviates
> `` (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] (` f · (` f · ` x)))) `` and not `` (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] (` f · (` f · ` x)))) `` and not
> `` (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] ` f)) · (` f · ` x) ``. `` (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] ` f)) · (` f · ` x) ``.
\begin{code} \begin{code}
ex₁ : (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹 ≡ (𝔹 ⇒ 𝔹) ⇒ (𝔹 ⇒ 𝔹) ex₁ : (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹 ≡ (𝔹 ⇒ 𝔹) ⇒ (𝔹 ⇒ 𝔹)
@ -530,9 +527,9 @@ data _⟹_ : Term → Term → Set where
We use the following special characters We use the following special characters
⟹ U+27F9: LONG RIGHTWARDS DOUBLE ARROW (\r6) ⟹ U+27F9: LONG RIGHTWARDS DOUBLE ARROW (\r6)
ξ U+03BE: GREEK SMALL LETTER XI (\Gx or \xi) ξ U+03BE: GREEK SMALL LETTER XI (\Gx or \xi)
β U+03B2: GREEK SMALL LETTER BETA (\Gb or \beta) β U+03B2: GREEK SMALL LETTER BETA (\Gb or \beta)
#### Quiz #### Quiz