diff options
| -rw-r--r-- | sec/encoding.ltx | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index b7029f3..c87ce90 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -472,14 +472,15 @@ the representation \(i_\ell\) of each label \(\ell\). Thus a tuple x. \casetm{x}{i_\ell}{\mathsf{inj}~\ell~t_\ell}{\ell})\). The projection \(t.\ell\) is encoded as the application \(\mathsf{prj}~(t~i_\ell)~\ell\). -At this phase the encodings of our example functions, -\systemtinline{balanced} and \systemtinline{compose'}, become too -cluttered to be useful. Instead we will consider the +Our example functions \systemtinline{balanced} and +\systemtinline{compose} use too many products to be illustrative +examples of this encoding at work. Instead we will consider the \systemtinline{dupfirst} function, of type \((\nat \to \nat) \times \nat \to (\nat \to \nat) \times (\nat \to \nat) \times \nat\), which takes a pair of a function and value, and duplicates the first component of the pair. -Originally defined as \systemtinline{let dupfirst t = (t.0, t.0, t.1)}, -after encoding products the function becomes +Originally defined as +\systemtinline{let dupfirst t = (t.0, t.0, t.1)}, after encoding +products the function becomes \begin{listing}[H] \begin{systemt} let dupfirst t = fun x => match x with |