helm/ocaml/cic_notation/doc/main.tex

   1 \documentclass[a4paper,draft]{article}
   2
   3 \usepackage{manfnt}
   4 \usepackage{a4wide}
   5 \usepackage{pifont}
   6 \usepackage{semantic}
   7 \usepackage{stmaryrd,latexsym}
   8
   9 \newcommand{\BLOB}{\raisebox{0ex}{\small\manstar}}
  10
  11 \newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}}
  12
  13 \title{Extensible notation for \MATITA}
  14 \author{Luca Padovani \qquad Stefano Zacchiroli \\
  15 \small Department of Computer Science, University of Bologna \\
  16 \small Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY \\
  17 \small \{\texttt{lpadovan}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}}
  18
  19 \newcommand{\BREAK}{\mathtt{break}}
  20 \newcommand{\TVAR}[1]{#1:\mathtt{term}}
  21 \newcommand{\IMPVAR}{\TVAR{\_}}
  22 \newcommand{\NVAR}[1]{#1:\mathtt{number}}
  23 \newcommand{\IVAR}[1]{#1:\mathtt{name}}
  24 \newcommand{\FENCED}[1]{\texttt{\char'050}#1\texttt{\char'051}}
  25 \newcommand{\ITO}[2]{|[#1|]_{\mathcal#2}^1}
  26 \newcommand{\IOT}[2]{|[#1|]_{#2}^2}
  27 \newcommand{\IAP}[2]{|[#1|]_{#2}^a}
  28 \newcommand{\IAPP}[3]{|[#1|]_{#2,#3}^a}
  29 \newcommand{\ADDPARENS}[2]{\llparenthesis#1\rrparenthesis^{#2}}
  30 \newcommand{\NAMES}{\mathit{names}}
  31 \newcommand{\DOMAIN}{\mathit{domain}}
  32 \newcommand{\UPDATE}[2]{#1[#2]}
  33
  34 \mathlig{~>}{\leadsto}
  35 \mathlig{|->}{\mapsto}
  36
  37 \begin{document}
  38   \maketitle
  39
  40   \input{body}
  41
  42 \end{document}
  43