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

More: improves readability of signatures for ext and rename (#537)

Browse source
This commit is contained in:
Marko Dimjašević 2020-10-24 17:01:30 +02:00 committed by GitHub
parent 2db6d7754f
commit 0aff7d8b2d
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/plfa/part2/More.lagda.md
View file

@ -737,11 +737,17 @@ count {∅} _ = ⊥-elim impossible
## Renaming
```
ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ∋ B)
ext : ∀ {Γ Δ}
→ (∀ {A} → Γ ∋ A → Δ ∋ A)
---------------------------------
→ (∀ {A B} → Γ , A ∋ B → Δ , A ∋ B)
ext ρ Z = Z
ext ρ (S x) = S (ρ x)
rename : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
rename : ∀ {Γ Δ}
→ (∀ {A} → Γ ∋ A → Δ ∋ A)
-----------------------
→ (∀ {A} → Γ ⊢ A → Δ ⊢ A)
rename ρ (` x) = ` (ρ x)
rename ρ (ƛ N) = ƛ (rename (ext ρ) N)
rename ρ (L · M) = (rename ρ L) · (rename ρ M)