diff options
| -rw-r--r-- | sec/lang.ltx | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/sec/lang.ltx b/sec/lang.ltx index a3d2cb7..da85b80 100644 --- a/sec/lang.ltx +++ b/sec/lang.ltx @@ -142,12 +142,12 @@ As a concrete example, consider the type \(\mathsf{Tree} \coloneq \mu X. 1 + (X X)\) of unlabeled binary trees. By combining injections with \roll{}, we can form two constructors of this type: \begin{align*} - \mathsf{leaf} &\coloneq \roll~\tuple{0, \tuple{}} &&: \mathsf{Tree} \\ - \mathsf{branch} &\coloneq \lambda x. \roll~\tuple{1, x} &&: \mathsf{Tree} \times \mathsf{Tree} \to \mathsf{Tree} + \mathsf{leaf} &\coloneq \roll~(\mathsf{Leaf}~\tuple{}) &&: \mathsf{Tree} \\ + \mathsf{branch} &\coloneq \lambda x. \roll~(\mathsf{Branch}~x) &&: \mathsf{Tree} \times \mathsf{Tree} \to \mathsf{Tree} \end{align*} and given a base case \(l : A\) and accumulator \(r : A \times A \to A\), we can fold over a tree \(t\) with the term -\[ \dofold{t}{x}{\domatch{x}{\tuple{0,\tuple{}}. l; \tuple{1,y}. r~y}} \] +\[ \dofold{t}{x}{\domatch{x}{\mathsf{Leaf}~\tuple{}. l; \mathsf{Branch}~y. r~y}} \] From the core of \lang{} we can further derive a number of useful operators. One of these is \mapkw, which lifts a function from type |