\nonstopmode
\documentclass{article}
\usepackage{pifont}
\usepackage[utf8x]{inputenc}

\usepackage{latex/agda}
\DeclareUnicodeCharacter{738}{$^\mathsf{s}$}
\DeclareUnicodeCharacter{8759}{::}

\setlength{\mathindent}{0pt}

\begin{document}
\begin{code}%
\>\<%
\\
\>\AgdaSymbol{\{-\#} \AgdaKeyword{OPTIONS} --copatterns --sized-types \AgdaSymbol{\#-\}}\<%
\\
%
\\
\>\AgdaKeyword{postulate}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaPostulate{Size} \<[9]%
\>[9]\AgdaSymbol{:} \AgdaPrimitiveType{Set}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaPostulate{Size<\_} \AgdaSymbol{:} \AgdaPostulate{Size} \AgdaSymbol{→} \AgdaPrimitiveType{Set}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaPostulate{↑\_} \<[9]%
\>[9]\AgdaSymbol{:} \AgdaPostulate{Size} \AgdaSymbol{→} \AgdaPostulate{Size}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaPostulate{∞} \<[9]%
\>[9]\AgdaSymbol{:} \AgdaPostulate{Size}\<%
\\
%
\\
\>\AgdaSymbol{\{-\#} \AgdaKeyword{BUILTIN} SIZE    \AgdaPostulate{Size} \<[27]%
\>[27]\AgdaSymbol{\#-\}}\<%
\\
\>\AgdaSymbol{\{-\#} \AgdaKeyword{BUILTIN} SIZELT  \AgdaPostulate{Size<\_} \AgdaSymbol{\#-\}}\<%
\\
\>\AgdaSymbol{\{-\#} \AgdaKeyword{BUILTIN} SIZESUC \AgdaPostulate{↑\_} \<[27]%
\>[27]\AgdaSymbol{\#-\}}\<%
\\
\>\AgdaSymbol{\{-\#} \AgdaKeyword{BUILTIN} SIZEINF \AgdaPostulate{∞} \<[27]%
\>[27]\AgdaSymbol{\#-\}}\<%
\\
%
\\
\>\AgdaKeyword{data} \AgdaDatatype{List} \AgdaSymbol{(}\AgdaBound{A} \AgdaSymbol{:} \AgdaPrimitiveType{Set}\AgdaSymbol{)} \AgdaSymbol{:} \AgdaPrimitiveType{Set} \AgdaKeyword{where}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaInductiveConstructor{[]} \AgdaSymbol{:} \AgdaDatatype{List} \AgdaBound{A}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaInductiveConstructor{\_∷\_} \AgdaSymbol{:} \AgdaSymbol{(}\AgdaBound{x} \AgdaSymbol{:} \AgdaBound{A}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaBound{xs} \AgdaSymbol{:} \AgdaDatatype{List} \AgdaBound{A}\AgdaSymbol{)} \AgdaSymbol{->} \AgdaDatatype{List} \AgdaBound{A}\<%
\\
%
\\
\>\AgdaKeyword{record} \AgdaRecord{\_×\_} \AgdaSymbol{(}\AgdaBound{A} \AgdaBound{B} \AgdaSymbol{:} \AgdaPrimitiveType{Set}\AgdaSymbol{)} \AgdaSymbol{:} \AgdaPrimitiveType{Set} \AgdaKeyword{where}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaKeyword{constructor} \AgdaInductiveConstructor{\_,\_}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaKeyword{field}\<%
\\
\>[2]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaField{fst} \AgdaSymbol{:} \AgdaBound{A}\<%
\\
\>[2]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaField{snd} \AgdaSymbol{:} \AgdaBound{B}\<%
\\
\>\AgdaKeyword{open} \AgdaModule{\_×\_}\<%
\\
%
\\
\>\AgdaComment{-- Sized streams via head/tail.}\<%
\\
%
\\
\>\AgdaKeyword{record} \AgdaRecord{Stream} \AgdaSymbol{\{}\AgdaBound{i} \AgdaSymbol{:} \AgdaPostulate{Size}\AgdaSymbol{\}} \AgdaSymbol{(}\AgdaBound{A} \AgdaSymbol{:} \AgdaPrimitiveType{Set}\AgdaSymbol{)} \AgdaSymbol{:} \AgdaPrimitiveType{Set} \AgdaKeyword{where}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaKeyword{coinductive}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaKeyword{constructor} \AgdaCoinductiveConstructor{\_∷\_}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaKeyword{field}\<%
\\
\>[2]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaField{head} \<[10]%
\>[10]\AgdaSymbol{:} \AgdaBound{A}\<%
\\
\>[2]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaField{tail} \<[10]%
\>[10]\AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{j} \AgdaSymbol{:} \AgdaPostulate{Size<} \AgdaBound{i}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaRecord{Stream} \AgdaSymbol{\{}\AgdaBound{j}\AgdaSymbol{\}} \AgdaBound{A}\<%
\\
\>\AgdaKeyword{open} \AgdaModule{Stream} \AgdaKeyword{public}\<%
\\
%
\\
\>\AgdaComment{-- Streams and lists.}\<%
\\
%
\\
\>\AgdaComment{-- Prepending a list to a stream.}\<%
\\
%
\\
\>\AgdaFunction{\_++ˢ\_} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{i} \AgdaBound{A}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaDatatype{List} \AgdaBound{A} \AgdaSymbol{→} \AgdaRecord{Stream} \AgdaSymbol{\{}\AgdaBound{i}\AgdaSymbol{\}} \AgdaBound{A} \AgdaSymbol{→} \AgdaRecord{Stream} \AgdaSymbol{\{}\AgdaBound{i}\AgdaSymbol{\}} \AgdaBound{A}\<%
\\
\>\AgdaInductiveConstructor{[]} \<[10]%
\>[10]\AgdaFunction{++ˢ} \AgdaBound{s} \AgdaSymbol{=} \AgdaBound{s}\<%
\\
\>\AgdaSymbol{(}\AgdaBound{a} \AgdaInductiveConstructor{∷} \AgdaBound{as}\AgdaSymbol{)} \<[10]%
\>[10]\AgdaFunction{++ˢ} \AgdaBound{s} \AgdaSymbol{=} \AgdaBound{a} \AgdaCoinductiveConstructor{∷} \AgdaSymbol{(}\AgdaBound{as} \AgdaFunction{++ˢ} \AgdaBound{s}\AgdaSymbol{)}\<%
\\
%
\\
\>\AgdaComment{-- Unfold which produces several outputs at one step}\<%
\\
%
\\
\>\AgdaKeyword{record} \AgdaRecord{List1} \AgdaSymbol{(}\AgdaBound{A} \AgdaSymbol{:} \AgdaPrimitiveType{Set}\AgdaSymbol{)} \AgdaSymbol{:} \AgdaPrimitiveType{Set} \AgdaKeyword{where}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaKeyword{constructor} \AgdaInductiveConstructor{\_∷\_}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaKeyword{field}\<%
\\
\>[2]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaField{first} \<[11]%
\>[11]\AgdaSymbol{:} \AgdaBound{A}\<%
\\
\>[2]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaField{rest} \<[11]%
\>[11]\AgdaSymbol{:} \AgdaDatatype{List} \AgdaBound{A}\<%
\\
\>\AgdaKeyword{open} \AgdaModule{List1} \AgdaKeyword{public}\<%
\\
%
\\
\>\AgdaFunction{unfold⁺} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{S} \AgdaSymbol{:} \AgdaPostulate{Size} \AgdaSymbol{→} \AgdaPrimitiveType{Set}\AgdaSymbol{\}} \AgdaSymbol{\{}\AgdaBound{A} \AgdaSymbol{:} \AgdaPrimitiveType{Set}\AgdaSymbol{\}}\<%
\\
%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaSymbol{(}\AgdaBound{step} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{i}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaBound{S} \AgdaBound{i} \AgdaSymbol{→} \AgdaRecord{List1} \AgdaBound{A} \AgdaRecord{×} \AgdaSymbol{(∀} \AgdaSymbol{\{}\AgdaBound{j} \AgdaSymbol{:} \AgdaPostulate{Size<} \AgdaBound{i}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaBound{S} \AgdaBound{j}\AgdaSymbol{))} \AgdaSymbol{→}\<%
\\
%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{i}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{s} \AgdaSymbol{:} \AgdaBound{S} \AgdaBound{i}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaRecord{Stream} \AgdaSymbol{\{}\AgdaBound{i}\AgdaSymbol{\}} \AgdaBound{A}\<%
\\
%
\\
\>\AgdaField{head} \<[6]%
\>[6]\AgdaSymbol{(}\AgdaFunction{unfold⁺} \AgdaBound{step} \AgdaBound{s}\AgdaSymbol{)} \AgdaSymbol{=} \<[26]%
\>[26]\AgdaField{first} \AgdaSymbol{(}\AgdaField{fst} \AgdaSymbol{(}\AgdaBound{step} \AgdaBound{s}\AgdaSymbol{))}\<%
\\
\>\AgdaField{tail} \<[6]%
\>[6]\AgdaSymbol{(}\AgdaFunction{unfold⁺} \AgdaBound{step} \AgdaBound{s}\AgdaSymbol{)} \AgdaSymbol{=} \<[26]%
\>[26]\AgdaKeyword{let} \<[31]%
\>[31]\AgdaSymbol{((\_} \AgdaInductiveConstructor{∷} \AgdaBound{l}\AgdaSymbol{)} \AgdaInductiveConstructor{,} \AgdaBound{s′}\AgdaSymbol{)} \AgdaSymbol{=} \AgdaBound{step} \AgdaBound{s}\<%
\\
\>[2]\AgdaIndent{26}{}\<[26]%
\>[26]\AgdaKeyword{in} \<[31]%
\>[31]\AgdaBound{l} \AgdaFunction{++ˢ} \AgdaFunction{unfold⁺} \AgdaBound{step} \AgdaBound{s′}\<%
\end{code}
Problem: The ∷ in the last let statement is not colored with constructor color.
\end{document}
