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

fix indentation on 736 to fix partial codeblocks

Browse source
This commit is contained in:
Altaria 2021-06-25 16:14:28 +01:00
parent 0f8be19802
commit dd370cd225
1 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/plfa/part2/Substitution.lagda.md
View file

@ -733,13 +733,13 @@ The proof is by induction on the term `M`.
* If `x = S y`, we obtain the goal by the following equational reasoning.
exts (exts σ) (ext ρ (S y))
≡ rename S_ (exts σ (ρ y))
≡ rename S_ (rename S_ (σ (ρ y) (by the premise)
≡ rename (ext ρ) (exts σ (S y)) (by compose-rename)
≡ rename ((ext ρ) ∘ S_) (σ y)
≡ rename (ext ρ) (rename S_ (σ y)) (by compose-rename)
≡ rename (ext ρ) (exts σ (S y))
exts (exts σ) (ext ρ (S y))
≡ rename S_ (exts σ (ρ y))
≡ rename S_ (rename S_ (σ (ρ y) (by the premise)
≡ rename (ext ρ) (exts σ (S y)) (by compose-rename)
≡ rename ((ext ρ) ∘ S_) (σ y)
≡ rename (ext ρ) (rename S_ (σ y)) (by compose-rename)
≡ rename (ext ρ) (exts σ (S y))
* If `M` is an application, we obtain the goal using the induction
hypothesis for each subterm.