1 files changed, 32 insertions, 0 deletions
diff --git a/content/zettel/3b3d.md b/content/zettel/3b3d.md
new file mode 100644
index 0000000..0b85ee0
--- /dev/null
+++ b/content/zettel/3b3d.md
@@ -0,0 +1,32 @@
++++
+title = "Subset Types and Variations"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3b3c"]
+forwardlinks = []
+zettelid = "3b3d"
++++
+
+`refine` can be used to define functions that take in and return subset
+types, by allowing you to replace placeholders with underscores, which
+can be proven afterwards. Together with powerful proof automation, this
+can be a nice way to define these dependent functions in a more similar
+way that they would be defined in Haskell or ML.
+
+However, `Program` is a term in Galina which can be used to prove these
+without `refine`, however, `refine` gives more control over how the
+proof is done.
+
+The `sumbool` type is the type that can return a proof of either type in
+it's constructor.
+
+`if then else` is actually overloaded in Coq and can work for any
+two-constructor `Inductive` type. This means it can be used with
+`sumbool` as well. When extracting `sumbool` to OCaml code, it uses
+`Left` and `Right` by default, however, it is better to use `true` and
+`false` in `bool` instead, which are built into OCaml. This can easily
+be done by telling Coq how it should extract the `sumbool` type.
+
+`sumor` is another type, which can either return a value of type A, or a
+proof of type B, which is written as the following: `A + {B}`.