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

Merge branch 'dev' of github.com:plfa/plfa.github.io into dev

Browse source
This commit is contained in:
wadler 2019-07-01 10:43:17 -03:00
commit cd5f1dd2d4
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/plfa/Lists.lagda
View file

@ -696,7 +696,7 @@ postulate
## Monoids ## Monoids
Typically when we use a fold the operator is associative and the Typically when we use a fold the operator is associative and the
value is a left and right identity for the value, meaning that the value is a left and right identity for the operator, meaning that the
operator and the value form a _monoid_. operator and the value form a _monoid_.
We can define a monoid as a suitable record type: We can define a monoid as a suitable record type:

8
src/plfa/Properties.lagda
View file

@ -476,9 +476,9 @@ With the extension lemma under our belts, it is straightforward to
prove renaming preserves types: prove renaming preserves types:
\begin{code} \begin{code}
rename : ∀ {Γ Δ} rename : ∀ {Γ Δ}
→ (∀ {x A} → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A) → (∀ {x A} → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A)
---------------------------------- ----------------------------------
→ (∀ {M A} → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A) → (∀ {M A} → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A)
rename ρ (⊢` ∋w) = ⊢` (ρ ∋w) rename ρ (⊢` ∋w) = ⊢` (ρ ∋w)
rename ρ (⊢ƛ ⊢N) = ⊢ƛ (rename (ext ρ) ⊢N) rename ρ (⊢ƛ ⊢N) = ⊢ƛ (rename (ext ρ) ⊢N)
rename ρ (⊢L · ⊢M) = (rename ρ ⊢L) · (rename ρ ⊢M) rename ρ (⊢L · ⊢M) = (rename ρ ⊢L) · (rename ρ ⊢M)
@ -498,7 +498,7 @@ the variable appears in `Δ`.
* If the term is a lambda abstraction, use the previous lemma to * If the term is a lambda abstraction, use the previous lemma to
extend the map `ρ` suitably and use induction to rename the body of the extend the map `ρ` suitably and use induction to rename the body of the
abstraction abstraction.
* If the term is an application, use induction to rename both the * If the term is an application, use induction to rename both the
function and the argument. function and the argument.