Add content

1 files changed, 18 insertions, 0 deletions

diff --git a/content/zettel/3b5a.md b/content/zettel/3b5a.md
new file mode 100644
index 0000000..0166a10
--- /dev/null
+++ b/content/zettel/3b5a.md
@@ -0,0 +1,18 @@
++++
+title = "Continuation passing style for `Ltac` functions"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3b5"]
+forwardlinks = []
+zettelid = "3b5a"
++++
+
+`Ltac` functions behave a lot like monads in Haskell, whereby they will
+be pure if no tactic has been invoked in them, but will be monadic if a
+tactic was executed before evaluating a `constr:()` construct. This is
+normally not a problem, as in Haskell there is the `return` function to
+lift any value into the monad.
+
+However, this is not defined for `Ltac`, and there is no `return`
+available.