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

fix typo

Browse source
This commit is contained in:
wadler 2020-08-07 09:05:37 +01:00
parent 91a2dd4bf8
commit 310c80a9bc
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
papers/scp/PLFA.tex
View file

@ -499,7 +499,7 @@ cases deal with the situation where there are potentially two
different reductions; each case is trivially shown to be
impossible. Five of the ten cases are redundant, as they just involve
switching the order of the arguments. We had to copy the cases
nsuitably permuted. It would be preferable to reinvoke the proof on
suitably permuted. It would be preferable to reinvoke the proof on
switched arguments, but this would not pass Agda's termination checker
since swapping the arguments doesn't yield a recursive call on
structurally smaller arguments. The proof of determinism in SF