From 7408a6b9aa210f06912d18cbf19b703446087c0a Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Fri, 25 Apr 2025 13:34:10 +0100 Subject: Give examples for phase 1. --- sec/encoding.ltx | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) (limited to 'sec/encoding.ltx') diff --git a/sec/encoding.ltx b/sec/encoding.ltx index a8d0269..6d339bd 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -99,7 +99,17 @@ Given a well-formedness derivation \(\jdgmnt{ty}{\Psi}{A}\), a type variable \(X \submult{A}{\sub{\alpha}{X/S \to S \times \alpha(X)}} \to S \to S \times \submult{A}{\alpha} \] that calls each accumulator within \(A\) in sequence. The definition is by -induction on the well-formedness derivation. +induction on the well-formedness derivation. At the end of this phase, the +\systemtinline{compose} example is unchanged. The \systemtinline{balanced} +example reduces to: +\begin{listing}[H] +\begin{systemt} +let balanced n f = primrec n with + Zero => roll2 [] (Leaf f) +| Suc tree => roll2 [tree, tree] (Branch (0, 1)) +\end{systemt} +\vspace{-\baselineskip} +\end{listing} \subsection{Phase 2: Encoding Inductive Types}% \label{subsec:inductive-types} -- cgit v1.2.3