Add content

1 files changed, 15 insertions, 0 deletions

diff --git a/content/zettel/3c3c2.md b/content/zettel/3c3c2.md
new file mode 100644
index 0000000..bfb08ba
--- /dev/null
+++ b/content/zettel/3c3c2.md
@@ -0,0 +1,15 @@
++++
+title = "Weakly embedded memoization"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3c3c1"]
+forwardlinks = ["3c3c3"]
+zettelid = "3c3c2"
++++
+
+Memoization can also be weakly embedded in Coq by using co-inductive
+datatypes. This works extremely well for functions that take Peano
+numbers as input, as a lazy data structure can be defined using
+co-inductive types, which represents unevaluated thunks. Once these are
+evaluated, they can just be read back normally.