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

a little more polishing

Browse source
This commit is contained in:
wadler 2018-04-20 17:25:28 -03:00
parent 9984b7b522
commit c31b90e9f0
2 changed files with 15 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Collections.lagda
View file

@ -79,13 +79,10 @@ module CollectionDec (A : Set) (_≟_ : ∀ (x y : A) → Dec (x ≡ y)) where
∈-[_] : ∀ {w x} → w ∈ [ x ] → w ≡ x
∈-[_] here = refl
∈-[_] (there ())
[_]-⊆ : ∀ {x xs} → [ x ] ⊆ x ∷ xs
[_]-⊆ w∈ rewrite ∈-[_] w∈ = here
≢-∷-to-∈ : ∀ {w x xs} → w ≢ x → w ∈ x ∷ xs → w ∈ xs
≢-∷-to-∈ w≢ here = ⊥-elim (w≢ refl)
≢-∷-to-∈ _ (there w∈) = w∈
there⁻¹ : ∀ {w x xs} → w ∈ x ∷ xs → w ≢ x → w ∈ xs
there⁻¹ here w≢ = ⊥-elim (w≢ refl)
there⁻¹ (there w∈) w≢ = w∈
there⟨_⟩ : ∀ {w x y xs} → w ∈ xs × w ≢ x → w ∈ y ∷ xs × w ≢ x
there⟨ ⟨ w∈ , w≢ ⟩ ⟩ = ⟨ there w∈ , w≢ ⟩

27
src/Typed.lagda
View file

@ -432,12 +432,9 @@ free-lemma (⊢L · ⊢M) w∈ with ++-to-⊎ w∈
ρ′ = ρ , x ↦ ` y
Σ′ : ∀ {w} → w ∈ xs′ → free (ρ′ w) ⊆ ys′
Σ′ {w} here with w ≟ x
... | yes refl = [_]-⊆
... | no w≢ = ⊥-elim (w≢ refl)
Σ′ {w} (there w∈) with w ≟ x
... | yes refl = [_]-⊆
... | no _ = there ∘ (Σ w∈)
Σ′ {w} w∈′ with w ≟ x
... | yes refl = ⊆-++₁
... | no w≢ = ⊆-++₂ ∘ Σ (there⁻¹ w∈′ w≢)
⊆xs′ : free N ⊆ xs′
⊆xs′ = \\-to-∷ ⊆xs
@ -448,12 +445,12 @@ free-lemma (⊢L · ⊢M) w∈ with ++-to-⊎ w∈
⊢ρ′ : ∀ {w C} → w ∈ xs′ → Γ′ ∋ w ⦂ C → Δ′ ⊢ ρ′ w ⦂ C
⊢ρ′ {w} _ Z with w ≟ x
... | yes _ = ` Z
... | no w≢x = ⊥-elim (w≢x refl)
⊢ρ′ {w} w∈′ (S w≢x ⊢w) with w ≟ x
... | yes refl = ⊥-elim (w≢x refl)
... | no w≢ = ⊥-elim (w≢ refl)
⊢ρ′ {w} w∈′ (S w≢ ⊢w) with w ≟ x
... | yes refl = ⊥-elim (w≢ refl)
... | no _ = ⊢rename {Δ} {Δ′} {ys} ⊢σ (Σ w∈) (⊢ρ w∈ ⊢w)
where
w∈ = ≢-∷-to-∈ w≢x w∈′
w∈ = there⁻¹ w∈′ w≢
⊢subst Σ ⊢ρ ⊆xs (⊢L · ⊢M)
= ⊢subst Σ ⊢ρ L⊆ ⊢L · ⊢subst Σ ⊢ρ M⊆ ⊢M
@ -481,11 +478,11 @@ free-lemma (⊢L · ⊢M) w∈ with ++-to-⊎ w∈
⊢ρ : ∀ {w B} → w ∈ xs → Γ′ ∋ w ⦂ B → Γ ⊢ ρ w ⦂ B
⊢ρ {w} w∈ Z with w ≟ x
... | yes _ = ⊢M
... | no w≢x = ⊥-elim (w≢x refl)
⊢ρ {w} w∈ (S w≢x ⊢w) with w ≟ x
... | yes refl = ⊥-elim (w≢x refl)
... | no _ = ` ⊢w
... | yes _ = ⊢M
... | no w≢ = ⊥-elim (w≢ refl)
⊢ρ {w} w∈ (S w≢ ⊢w) with w ≟ x
... | yes refl = ⊥-elim (w≢ refl)
... | no _ = ` ⊢w
⊆xs : free N ⊆ xs
⊆xs x∈ = x∈