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

fix typo in Confluence

Browse source
This commit is contained in:
wadler 2021-08-10 17:51:05 +01:00
parent 00a04e43d1
commit effcfb1e3e
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/plfa/part2/Confluence.lagda.md
View file

@ -611,7 +611,7 @@ confluence L↠M₁ L↠M₂
## Notes ## Notes
Broadly speaking, this proof of confluence, based on parallel Broadly speaking, this proof of confluence, based on parallel
reduction, is due to W. Tait and P. Martin-Löf (see Barendredgt 1984, reduction, is due to W. Tait and P. Martin-Löf (see Barendregt 1984,
Section 3.2). Details of the mechanization come from several sources. Section 3.2). Details of the mechanization come from several sources.
The `subst-par` lemma is the "strong substitutivity" lemma of Shafer, The `subst-par` lemma is the "strong substitutivity" lemma of Shafer,
Tebbi, and Smolka (ITP 2015). The proofs of `par-triangle`, `strip`, Tebbi, and Smolka (ITP 2015). The proofs of `par-triangle`, `strip`,