\documentclass{article}
\input camila.mac
\usepackage{fullpage}
\begin{document}

$\begin{array}{l}
intAvg:{INT^{\star}} \times INT \tfunc{INT} \\ intAvg(l,p) \deff \\ \rule{3ex}{0pt}  
\LET 
a = 
length(l)\\
b = 
{
intSUM(l) \times 
intPot(10,p)} 
\IN 
{b / a} 
\TEL
\end{array}$

\traco

$\begin{array}{l}
intSUM:{INT^{\star}} \tfunc{INT} \\ intSUM(l) \deff \\ \rule{3ex}{0pt}  add-red(0,l)
\end{array}$

\traco

$\begin{array}{l}
intMIN:{\set{INT}} \tfunc{INT} \\ intMIN(s) \deff \\ \rule{3ex}{0pt}  min-red(32767,s)
\end{array}$

\traco

$\begin{array}{l}
intMAX:{\set{INT}} \tfunc{INT} \\ intMAX(s) \deff \\ \rule{3ex}{0pt}  max-red(0,s)
\end{array}$

\traco

$\begin{array}{l}
intMUL:{INT^{\star}} \tfunc{INT} \\ intMUL(l) \deff \\ \rule{3ex}{0pt}  mul-red(1,l)
\end{array}$

\traco

$\begin{array}{l}
intPot:INT \times INT \tfunc{INT} \\ intPot(a,b) \deff \\ \rule{3ex}{0pt}  
\LET 
l = \enlist{a \asor i \in 
inseg(b)} 
\IN 
intMUL(l) 
\TEL
\end{array}$

\traco

$\begin{array}{l}
intSet2IncIntSeq:{\set{INT}} \tfunc{{INT^{\star}}} \\ intSet2IncIntSeq(s) \deff \\ \rule{3ex}{0pt}  
\COND{
s = \emptyset}{\emptylist}{
\LET 
m = 
intMIN(s)\\
t = \{x \asor x \in s \wedge 
{x \neq m}\} 
\IN \enlist{m} \conc 
intSet2IncIntSeq(t) 
\TEL}
\end{array}$

\traco

$\begin{array}{l}
intSet2IntSeq:{\set{INT}} \tfunc{{INT^{\star}}} \\ intSet2IntSeq(s) \deff \\ \rule{3ex}{0pt}  
\COND{
s = \emptyset}{\emptylist}{
\LET 
m = 
intMAX(s)\\
t = \{x \asor x \in s \wedge 
{x \neq m}\} 
\IN \enlist{m} \conc 
intSet2IntSeq(t) 
\TEL}
\end{array}$

\traco

$\begin{array}{l}
intFF2index:A \pfunc{INT} \tfunc{{A^{\star}}} \\ intFF2index(ff) \deff \\ \rule{3ex}{0pt}  
\COND{
ff = \left( \begin{array}{c}
  \\  
\end{array} \right)}{\emptylist}{
\LET 
m = 
intMIN(
ran(ff))\\
X = \{a \asor a \in 
dom(ff) \wedge 

ff(a) = m\}\\
l = \enlist{a \asor a \in X} 
\IN l \conc 
intFF2index(
{ff \mapds X}) 
\TEL}
\end{array}$

\traco

$\begin{array}{l}
intAsRealRound:INT \times INT \tfunc{INT} \\ intAsRealRound(n,i) \deff \\ \rule{3ex}{0pt}  
\LET 
p = 
intPot(10,i)\\
d = 
{n / p}\\
r = 
rem(n,p) 
\IN 
\COND{
{r < 
{p / 2}}}{d}{
{d + 1}} 
\TEL
\end{array}$

\traco

$\begin{array}{l}
intAsReal2STR:INT \times INT \tfunc{STR} \\ intAsReal2STR(i,d) \deff \\ \rule{3ex}{0pt}  
\LET 
x = 
intPot(10,d)\\
d = 
div(i,x)\\
r = 
rem(i,x) 
\IN 
strcat(
itoa(d),\mattt{
\mbox{\texttt{"."}}},
itoa(r)) 
\TEL
\end{array}$

\traco
\end{document}
