From 310c80a9bcc5fe7be1f60207f5a041f604ecdd8f Mon Sep 17 00:00:00 2001 From: wadler Date: Fri, 7 Aug 2020 09:05:37 +0100 Subject: [PATCH] fix typo --- papers/scp/PLFA.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/papers/scp/PLFA.tex b/papers/scp/PLFA.tex index cd74ac64..1c6196cf 100755 --- a/papers/scp/PLFA.tex +++ b/papers/scp/PLFA.tex @@ -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