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

$\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(  \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}
intPerc:int \times int \times int \tfunc{int} \\ intPerc(x,y,i) \deff \\ \rule{3ex}{0pt}  
\LET 
p = 
intPot(10,
i + 2) 
\IN 

x \times p / y 
\TEL
\end{array}$

\traco

$\begin{array}{l}
intAsReal2STR:int \times int \tfunc{str} \\ intAsReal2STR(x,i) \deff \\ \rule{3ex}{0pt}  
\COND{
i = 0}{
itoa(x)}{
\LET 
n = 
\COND{
x < 0}{
0 - x}{x}\\
dig = 
\LAMBDA{i,n}
rem(
div(n,
intPot(10,
i - 1)),10)\\
r = 
seqInv(\enlist{
dig(j,n) \asor j \in 
\inseg{i}}) 
\IN 
\COND{
x < 0}{\!\!\mattt{
\mbox{\texttt{"-"}}}}{\!\!\mattt{
""}} \conc 
itoa(
div(n,
intPot(10,i))) \conc \!\!\mattt{
\mbox{\texttt{"."}}} \conc 
strCAT( 
itoa^* (r)) 
\TEL}
\end{array}$

\traco

$\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
\end{document}
