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

fixed backticks in code spans

Browse source
This commit is contained in:
Philip Wadler 2017-07-14 10:56:59 +01:00
parent 3de139a5ef
commit a43bdb46c7
4 changed files with 4851 additions and 4851 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3632
out/Stlc.md
View file

File diff suppressed because it is too large Load diff

6218
out/StlcProp.md
View file

File diff suppressed because it is too large Load diff

4
src/Stlc.lagda
View file

@ -70,7 +70,7 @@ data Type : Set where
\end{code} \end{code}
Terms have six constructs. Three are for the core lambda calculus: Terms have six constructs. Three are for the core lambda calculus:
* Variables, `\` x` * Variables, `` ` x ``
* Abstractions, `λ[ x ∶ A ] N` * Abstractions, `λ[ x ∶ A ] N`
* Applications, `L · M` * Applications, `L · M`
and three are for the base type, booleans: and three are for the base type, booleans:
@ -285,7 +285,7 @@ outermost term is now `if_then_else_`, which is typed using `𝔹-E`. The
?2 : ∅ , x ∶ 𝔹 ⊢ true ∶ 𝔹 ?2 : ∅ , x ∶ 𝔹 ⊢ true ∶ 𝔹
Again we fill in the three holes by typing C-c C-r in each. Agda observes Again we fill in the three holes by typing C-c C-r in each. Agda observes
that `\` x`, `false`, and `true` are typed using `Ax`, `𝔹-I₂`, and that `` ` x ``, `false`, and `true` are typed using `Ax`, `𝔹-I₂`, and
`𝔹-I₁` respectively. The `Ax` rule in turn takes an argument, to show `𝔹-I₁` respectively. The `Ax` rule in turn takes an argument, to show
that `(∅ , x ∶ 𝔹) x = just 𝔹`, which can in turn be specified with a that `(∅ , x ∶ 𝔹) x = just 𝔹`, which can in turn be specified with a
hole. After filling in all holes, the term is as above. hole. After filling in all holes, the term is as above.

4
src/StlcProp.lagda
View file

@ -266,7 +266,7 @@ _Proof_: We show, by induction on the proof that `x` appears
free in `M`, that, for all contexts `Γ`, if `M` is well free in `M`, that, for all contexts `Γ`, if `M` is well
typed under `Γ`, then `Γ` assigns some type to `x`. typed under `Γ`, then `Γ` assigns some type to `x`.
- If the last rule used was `free-\``, then `M = \` x`, and from - If the last rule used was `` free-` ``, then `M = `` `x ``, and from
the assumption that `M` is well typed under `Γ` we have the assumption that `M` is well typed under `Γ` we have
immediately that `Γ` assigns a type to `x`. immediately that `Γ` assigns a type to `x`.
@ -452,7 +452,7 @@ we show that if `∅ ⊢ V ∶ A` then `Γ ⊢ N [ x := V ] ∶ B`.
- If `N` is a variable there are two cases to consider, - If `N` is a variable there are two cases to consider,
depending on whether `N` is `x` or some other variable. depending on whether `N` is `x` or some other variable.
- If `N = \` x`, then from `Γ , x ∶ A ⊢ x ∶ B` - If `N = `` `x ``, then from `Γ , x ∶ A ⊢ x ∶ B`
we know that looking up `x` in `Γ , x : A` gives we know that looking up `x` in `Γ , x : A` gives
`just B`, but we already know it gives `just A`; `just B`, but we already know it gives `just A`;
applying injectivity for `just` we conclude that `A ≡ B`. applying injectivity for `just` we conclude that `A ≡ B`.