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

De Bruijn: changes the alignment of function arguments for consistency

Browse source
This commit is contained in:
Marko Dimjašević 2020-10-02 13:33:42 +02:00
parent 849807da58
commit 41d7e373ce
No known key found for this signature in database
GPG key ID: 565EE9641503F0AA
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/plfa/part2/DeBruijn.lagda.md
View file

@ -692,10 +692,10 @@ variables it is easy to define the special case of
substitution for one free variable: substitution for one free variable:
``` ```
_[_] : ∀ {Γ A B} _[_] : ∀ {Γ A B}
→ Γ , B ⊢ A → Γ , B ⊢ A
→ Γ ⊢ B → Γ ⊢ B
--------- ---------
→ Γ ⊢ A → Γ ⊢ A
_[_] {Γ} {A} {B} N M = subst {Γ , B} {Γ} σ {A} N _[_] {Γ} {A} {B} N M = subst {Γ , B} {Γ} σ {A} N
where where
σ : ∀ {A} → Γ , B ∋ A → Γ ⊢ A σ : ∀ {A} → Γ , B ∋ A → Γ ⊢ A