Annotation of /branches/pure-cfg/doc/typing/defs.tex

Parent Directory | Revision Log

---

Revision 477 - (view) (download) (as text)

1 :	jhr	64	%!TEX root = typing.tex
2 :			%
3 :
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	64	\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 :			\newcommand{\point}{\textbullet~}
42 :
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 :	jhr	66	\newcommand{\TYconst}{\iota}
108 :	jhr	64	\newcommand{\TYbool}{\mathbf{bool}}
109 :			\newcommand{\TYint}{\mathbf{int}}
110 :			\newcommand{\TYreal}{\mathbf{real}}
111 :			\newcommand{\TYrawten}[2]{\mathbf{rawten}\langle{}#1,#2\rangle{}}
112 :			\newcommand{\TYtensor}[1]{\mathbf{tensor}\langle{}#1\rangle{}}
113 :			\newcommand{\TYmatrix}[2]{\mathbf{matrix}\langle{}#1,#2\rangle{}}
114 :			\newcommand{\TYimage}[2]{\mathbf{image}_{#1}\langle{}#2\rangle{}}
115 :			\newcommand{\TYkern}[1]{\mathbf{kern}^{#1}}
116 :			\newcommand{\TYfield}[3]{\mathbf{field}^{#1}_{#2}\langle{}#3\rangle{}}
117 :			\newcommand{\TYvec}[1]{\mathbf{vec}_{#1}}
118 :
119 :			\newcommand{\Seq}[1]{\vec{#1}}
120 :
121 :			% Diderot operators
122 :			%
123 :			\newcommand{\OP}[1]{\mkw{#1}}
124 :			\newcommand{\OPdiff}{\OP{D}}
125 :			\newcommand{\OPconvolve}{\OP{convolve}}
126 :
127 :	jhr	66	% unification
128 :			%
129 :	jhr	67	\newcommand{\U}[2]{\mathcal{U}(#1,\,#2)}
130 :	jhr	66
131 :	jhr	64	% typing judgments
132 :			%
133 :			\newcommand{\HasTy}[2]{#1 : #2}
134 :			\newcommand{\UnopTy}[3]{\HasTy{#1}{#2 \rightarrow #3}}
135 :			\newcommand{\BinopTy}[4]{\HasTy{#1}{#2 \times #3 \rightarrow #4}}
136 :

---

root@smlnj-gforge.cs.uchicago.edu	ViewVC Help
Powered by ViewVC 1.0.0