Add content

1 files changed, 19 insertions, 0 deletions

diff --git a/content/zettel/3b3b.md b/content/zettel/3b3b.md
new file mode 100644
index 0000000..63e06ee
--- /dev/null
+++ b/content/zettel/3b3b.md
@@ -0,0 +1,19 @@
++++
+title = "Reflexive Types"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3b3a"]
+forwardlinks = ["3b3c"]
+zettelid = "3b3b"
++++
+
+Reflexive types are of the nature of taking an argument which is a
+function and returning the Inductive type. Some of these are not legal
+in Coq, even though they would be legal in Haskell/ML, as they might
+produce computations that run forever. This would destroy all the
+confidence that one could have in the proof system, as that would mean
+that one could produce a proof for any theorem using an infinite loop.
+This can be done because proofs are combined with functions. For
+example, a reflexive type that takes the type it defines as an argument
+could recurse indefinitely, which should not be allowed to be defined.