lhs2tex-1.12: Examples/Calc.lhs

\documentclass{article}

%include polycode.fmt

% preparation, can go into preamble
\newcommand\calculationcomments{%
  \def\commentbegin{\{ }%
  \def\commentend{\}}}%

%space adjustment, can also be defined globally:
%format ^^^ = "\quad "

\begin{document}

%concrete calculation example:
\begingroup% keep comment change local to group
\calculationcomments
\begin{spec}
   2 * (sum (Succ n'))
=  ^^^  {- definition of sum -}
   2 * ((Succ n') + (sum n'))
=       {- distributivity -}
   2 * (Succ n') + 2 * (sum n')
=       {- IH -}
   2 * (Succ n') + n * (Succ n')
=       {- distributivity -}
   (2 + n) * (Succ n')
=       {- commutativity, definition of + -}
   (Succ n') * (Succ (Succ n'))
\end{spec}
\endgroup

\end{document}