| 1 : |
jhr |
44 |
%!TEX root = diderot.tex
|
| 2 : |
|
|
%
|
| 3 : |
jhr |
16 |
|
| 4 : |
|
|
\usepackage{times}
|
| 5 : |
|
|
%-------------------------
|
| 6 : |
|
|
% the following magic makes the tt font in math mode be the same as the
|
| 7 : |
|
|
% normal tt font (i.e., Courier)
|
| 8 : |
|
|
%
|
| 9 : |
jhr |
380 |
\SetMathAlphabet{\mathtt}{normal}{OT1}{pcr}{m}{n}
|
| 10 : |
jhr |
16 |
\SetMathAlphabet{\mathtt}{bold}{OT1}{pcr}{bx}{n}
|
| 11 : |
|
|
%-------------------------
|
| 12 : |
|
|
|
| 13 : |
|
|
\usepackage{amsmath}
|
| 14 : |
|
|
|
| 15 : |
|
|
\newcommand{\NOTE}[1]{%
|
| 16 : |
|
|
\par\leavevmode\noindent\textbf{[[ #1 ]]}\par\leavevmode\noindent}
|
| 17 : |
|
|
\newcommand{\CUT}[1]{}
|
| 18 : |
|
|
\newcommand{\SIDENOTE}[1]{%
|
| 19 : |
|
|
\marginpar{\tiny\raggedright{#1}}}
|
| 20 : |
|
|
|
| 21 : |
|
|
\newcommand{\appref}[1]{Appendix~\ref{#1}}
|
| 22 : |
|
|
\newcommand{\chapref}[1]{Chapter~\ref{#1}}
|
| 23 : |
|
|
\newcommand{\secref}[1]{Section~\ref{#1}}
|
| 24 : |
|
|
\newcommand{\tblref}[1]{Table~\ref{#1}}
|
| 25 : |
|
|
\newcommand{\figref}[1]{Figure~\ref{#1}}
|
| 26 : |
|
|
\newcommand{\listingref}[1]{Listing~\ref{#1}}
|
| 27 : |
|
|
\newcommand{\pref}[1]{{page~\pageref{#1}}}
|
| 28 : |
|
|
\newcommand{\defref}[1]{Definition~\ref{#1}}
|
| 29 : |
|
|
\newcommand{\ruleref}[1]{Rule~\ref{#1}}
|
| 30 : |
|
|
|
| 31 : |
|
|
\newcommand{\eg}{{\em e.g.}}
|
| 32 : |
|
|
\newcommand{\cf}{{\em cf.}}
|
| 33 : |
|
|
\newcommand{\ie}{{\em i.e.}}
|
| 34 : |
|
|
\newcommand{\etc}{{\em etc.\/}}
|
| 35 : |
|
|
\newcommand{\naive}{na\"{\i}ve}
|
| 36 : |
|
|
\newcommand{\ala}{{\em \`{a} la\/}}
|
| 37 : |
|
|
\newcommand{\etal}{{\em et al.\/}}
|
| 38 : |
|
|
\newcommand{\role}{r\^{o}le}
|
| 39 : |
|
|
\newcommand{\vs}{{\em vs.}}
|
| 40 : |
|
|
\newcommand{\forte}{{fort\'{e}\/}}
|
| 41 : |
glk |
22 |
\newcommand{\point}{\textbullet~}
|
| 42 : |
jhr |
16 |
|
| 43 : |
|
|
%
|
| 44 : |
|
|
% font commands
|
| 45 : |
|
|
\providecommand{\bftt}[1]{{\ttfamily\bfseries{}#1}}
|
| 46 : |
|
|
\providecommand{\ittt}[1]{{\ttfamily\itshape{}#1}}
|
| 47 : |
|
|
\providecommand{\kw}[1]{\bftt{#1}}
|
| 48 : |
|
|
\providecommand{\nt}[1]{{\rmfamily\itshape{#1}}}
|
| 49 : |
|
|
\providecommand{\term}[1]{{\sffamily{#1}}}
|
| 50 : |
|
|
\providecommand{\tyvar}[1]{\ittt{#1}}
|
| 51 : |
|
|
%
|
| 52 : |
|
|
% math-mode versions
|
| 53 : |
|
|
\providecommand{\mkw}[1]{\ensuremath{\text{\kw{#1}}}}
|
| 54 : |
|
|
\providecommand{\mnt}[1]{\ensuremath{\text{\nt{#1}}}}
|
| 55 : |
|
|
\providecommand{\mterm}[1]{\ensuremath{\text{\term{#1}}}}
|
| 56 : |
|
|
\providecommand{\mtyvar}[1]{\ensuremath{\text{\tyvar{#1}}}}
|
| 57 : |
|
|
|
| 58 : |
|
|
% braces (in math mode)
|
| 59 : |
|
|
\newcommand{\LCB}{\mkw{\{}}
|
| 60 : |
|
|
\newcommand{\RCB}{\mkw{\}}}
|
| 61 : |
|
|
|
| 62 : |
|
|
% underscore
|
| 63 : |
|
|
\newcommand{\US}{\char`\_}
|
| 64 : |
|
|
|
| 65 : |
|
|
%%%%%
|
| 66 : |
|
|
% Some common math notation
|
| 67 : |
|
|
%
|
| 68 : |
|
|
|
| 69 : |
|
|
% double brackets
|
| 70 : |
|
|
\newcommand{\LDB}{\ensuremath{[\mskip -3mu [}}
|
| 71 : |
|
|
\newcommand{\RDB}{\ensuremath{]\mskip -3mu ]}}
|
| 72 : |
|
|
|
| 73 : |
|
|
\newcommand{\dom}{\ensuremath{\mathrm{dom}}}
|
| 74 : |
|
|
\newcommand{\rng}{\ensuremath{\mathrm{rng}}}
|
| 75 : |
|
|
|
| 76 : |
|
|
% sets
|
| 77 : |
|
|
\newcommand{\SET}[1]{\ensuremath{\{#1\}}}
|
| 78 : |
|
|
\newcommand{\Fin}{\textrm{Fin}} % finite power set
|
| 79 : |
|
|
\newcommand{\DISJOINT}[2]{\ensuremath{#1 \pitchfork #2}}
|
| 80 : |
|
|
\newcommand{\finsubset}{\mathrel{\stackrel{\textrm{fin}}{\subset}}}
|
| 81 : |
|
|
|
| 82 : |
|
|
% finite maps
|
| 83 : |
|
|
\newcommand{\finmap}{\mathrel{\stackrel{\textrm{fin}}{\rightarrow}}}
|
| 84 : |
|
|
\newcommand{\MAP}[2]{\SET{#1 \mapsto #2}}
|
| 85 : |
|
|
\newcommand{\EXTEND}[2]{\ensuremath{#1{\pm}#2}}
|
| 86 : |
|
|
\newcommand{\EXTENDone}[3]{\EXTEND{#1}{\MAP{#2}{#3}}}
|
| 87 : |
|
|
\newcommand{\SUBST}[3]{\ensuremath{#1[#2\mapsto{}#3]}}
|
| 88 : |
|
|
\newcommand{\SUBSTTWO}[5]{\ensuremath{#1[#2\mapsto{}#3,#4\mapsto{}#5]}}
|
| 89 : |
|
|
|
| 90 : |
|
|
% inference rules
|
| 91 : |
|
|
\newcommand{\infer}[2]{\frac{\;{#2}\;}{\;{#1}\;}}
|
| 92 : |
|
|
%
|
| 93 : |
|
|
% labeled inference rule:
|
| 94 : |
|
|
% \INFER{name}{label}{conclusion}{assumption}
|
| 95 : |
|
|
%
|
| 96 : |
|
|
\newcommand{\INFER}[2]{%
|
| 97 : |
|
|
\begin{equation*}
|
| 98 : |
|
|
\infer{#1}{#2}
|
| 99 : |
|
|
\end{equation*}}
|
| 100 : |
|
|
|
| 101 : |
|
|
% natural numbers
|
| 102 : |
|
|
%
|
| 103 : |
|
|
\newcommand{\Nat}{\mathcal{N}}
|
| 104 : |
|
|
|
| 105 : |
|
|
% Diderot types
|
| 106 : |
|
|
%
|
| 107 : |
|
|
\newcommand{\TYbool}{\mathbf{bool}}
|
| 108 : |
|
|
\newcommand{\TYint}{\mathbf{int}}
|
| 109 : |
|
|
\newcommand{\TYreal}{\mathbf{real}}
|
| 110 : |
jhr |
43 |
\newcommand{\TYrawten}[2]{\mathbf{rawten}\langle{}#1,#2\rangle{}}
|
| 111 : |
|
|
\newcommand{\TYtensor}[1]{\mathbf{tensor}\langle{}#1\rangle{}}
|
| 112 : |
jhr |
16 |
\newcommand{\TYmatrix}[2]{\mathbf{matrix}\langle{}#1,#2\rangle{}}
|
| 113 : |
|
|
\newcommand{\TYimage}[2]{\mathbf{image}_{#1}\langle{}#2\rangle{}}
|
| 114 : |
|
|
\newcommand{\TYkern}[1]{\mathbf{kern}^{#1}}
|
| 115 : |
|
|
\newcommand{\TYfield}[3]{\mathbf{field}^{#1}_{#2}\langle{}#3\rangle{}}
|
| 116 : |
|
|
\newcommand{\TYvec}[1]{\mathbf{vec}_{#1}}
|
| 117 : |
|
|
|
| 118 : |
jhr |
43 |
\newcommand{\Seq}[1]{\vec{#1}}
|
| 119 : |
|
|
|
| 120 : |
jhr |
16 |
% Diderot operators
|
| 121 : |
|
|
%
|
| 122 : |
jhr |
44 |
\newcommand{\OP}[1]{\mkw{#1}}
|
| 123 : |
|
|
\newcommand{\OPdiff}{\OP{D}}
|
| 124 : |
|
|
\newcommand{\OPconvolve}{\OP{convolve}}
|
| 125 : |
jhr |
16 |
|
| 126 : |
|
|
% typing judgments
|
| 127 : |
|
|
%
|
| 128 : |
|
|
\newcommand{\HasTy}[2]{#1 : #2}
|
| 129 : |
|
|
\newcommand{\UnopTy}[3]{\HasTy{#1}{#2 \rightarrow #3}}
|
| 130 : |
|
|
\newcommand{\BinopTy}[4]{\HasTy{#1}{#2 \times #3 \rightarrow #4}}
|
| 131 : |
|
|
|
Parent Directory
| 
Revision Log
