From 0aff7d8b2dc360beea70d632c3e2a6e54640e384 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Sat, 24 Oct 2020 17:01:30 +0200 Subject: [PATCH] More: improves readability of signatures for ext and rename (#537) --- src/plfa/part2/More.lagda.md | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/plfa/part2/More.lagda.md b/src/plfa/part2/More.lagda.md index 548ad58a..6a46f4bb 100644 --- a/src/plfa/part2/More.lagda.md +++ b/src/plfa/part2/More.lagda.md @@ -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)