diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-05-11 19:38:03 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-11 19:38:03 +0100 |
commit | 47c1289ff658a5aec71635d79ffe30bb29a07876 (patch) | |
tree | 56cf6b959e37fed88c492d34defd3d7ec40e7148 /content/zettel/3b3d.md | |
parent | fbe0fc62120348f582dc4db2b614078943d0764b (diff) | |
download | zk-web-47c1289ff658a5aec71635d79ffe30bb29a07876.tar.gz zk-web-47c1289ff658a5aec71635d79ffe30bb29a07876.zip |
Add content
Diffstat (limited to 'content/zettel/3b3d.md')
-rw-r--r-- | content/zettel/3b3d.md | 32 |
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}`. |