+++
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.