blob: 0166a109ebfeaf297565818c7cf9adcf2651a26e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
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.
|
