Correspondence: note divergence

Blaisorblade · Mar 4, 2020 · 4d94a80 · 4d94a80
1 parent 19b38b9
commit 4d94a80
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/correspondence.md b/correspondence.md
@@ -21,6 +21,9 @@ All file paths in this file are relative to the `theories/` folder.
 - Covariant lists example: `Dot/examples/list.v`.
 - Positive integers example: `Dot/examples/examples.v`.
 - Unsafe motivating example: `Dot/examples/fromPDotMutualRecSem.v`.
+- Earlier variant from Sec. 1: `Dot/examples/fromPDotMutualRec.v`; here we
+  simplified the use of `Option` away, which we preserve in
+  `Dot/examples/fromPDotMutualRecSem.v`.
 
 - For the code sizes reported in Sec. 6, see `codesize.md`.