preamble.tex

\usepackage[intlimits]{amsmath}
\usepackage{amsfonts,amssymb}
\DeclareSymbolFontAlphabet{\mathbb}{AMSb}
\usepackage{natbib}
\usepackage{float}
\usepackage[bf]{caption}
\captionsetup{margin=0.5in}
\usepackage{fancyhdr}
%\usepackage{fancyheadings}
\usepackage{fancybox}
\usepackage{ifthen}
\usepackage{bu_ece_thesis}
\usepackage{url}
\usepackage{lscape,afterpage}
\usepackage{xspace}
\usepackage{epstopdf} 
\usepackage{subfig}
\usepackage[figuresleft]{rotating}
% \usepackage{bigfoot}
% from lyx.
\usepackage{xcolor}
\usepackage{array}
\usepackage{mathtools}
\usepackage{enumitem}
\usepackage{multirow}
\usepackage{cancel}
\usepackage{listings}
\renewcommand{\lstlistingname}{Listing}
\usepackage{amsthm}
\usepackage{wasysym}
\usepackage{makecell}
\usepackage{datetime2}


\PassOptionsToPackage{normalem}{ulem}
\usepackage{ulem}

% \usepackage[printonlyused,withpage]{acronym}
\usepackage{acro}

% graphicx and pdf creation
\usepackage{graphicx}
\usepackage{appendix}

% keep text from breaking the margins
\sloppy

% % keep footnotes from splitting across pages?
% \interfootnotelinepenalty=10000

% some voodoo from https://tex.stackexchange.com/questions/2651/should-i-use-center-or-centering-for-figures-and-tables
\makeatletter
\g@addto@macro\@floatboxreset\centering
\makeatother


\theoremstyle{plain}
\newtheorem{thm}{\protect\theoremname}[chapter] % this is consitent with the figures at least
\theoremstyle{plain}
\newtheorem{lem}[thm]{\protect\lemmaname}
\theoremstyle{plain}
\newtheorem{fact}[thm]{\protect\factname}
\theoremstyle{plain}
\newtheorem{cor}[thm]{\protect\corollaryname}
\newlist{casenv}{enumerate}{4}
\setlist[casenv]{leftmargin=*,align=left,widest={iiii}}
\setlist[casenv,1]{label={{\itshape\ \casename} \arabic*.},ref=\arabic*}
\setlist[casenv,2]{label={{\itshape\ \casename} \roman*.},ref=\roman*}
\setlist[casenv,3]{label={{\itshape\ \casename\ \alph*.}},ref=\alph*}
\setlist[casenv,4]{label={{\itshape\ \casename} \arabic*.},ref=\arabic*}
\theoremstyle{definition}
\newtheorem{example}[thm]{\protect\examplename}
\theoremstyle{plain}
\newtheorem{conjecture}[thm]{\protect\conjecturename}

\theoremstyle{remark}
\newtheorem{claim}[thm]{\protect\claimname}
% why isn't this bold?


\usepackage{xcolor}
\usepackage{tikz-cd}
\tikzcdset{%
    triple line/.code={\tikzset{%
        double equal sign distance, % replace by double distance = 'measure' 
        double=\pgfkeysvalueof{/tikz/commutative diagrams/background color}}},
    quadruple line/.code={\tikzset{%
        double equal sign distance, % replace by double distance = 'measure'
        double=\pgfkeysvalueof{/tikz/commutative diagrams/background color}}},
    Rrightarrow/.code={\tikzcdset{triple line}\pgfsetarrows{tikzcd implies cap-tikzcd implies}},
    RRightarrow/.code={\tikzcdset{quadruple line}\pgfsetarrows{tikzcd implies cap-tikzcd implies}}
}    

\newcommand*{\tarrow}[2][]{\arrow[Rrightarrow, #1]{#2}\arrow[dash, shorten >= 0.5pt, #1]{#2}}
\newcommand*{\tarrows}[2][]{\arrow[Rrightarrow, shorten >= 2.5pt, #1]{#2}\arrow[dash, shorten >= 3pt, #1]{#2}}

\newcommand*{\deqs}[2][]{\arrow[Rrightarrow, no head, #1]{#2}\arrow[dash, no head #1]{#2}}
\newcommand*{\qarrow}[2][]{\arrow[RRightarrow, #1]{#2}\arrow[equal, double distance = 0.25pt, shorten >= 1.28pt, #1]{#2}}

\makeatother

\usepackage{babel}

\providecommand{\conjecturename}{Conjecture}
\providecommand{\claimname}{Claim}
\providecommand{\casename}{Case}
\providecommand{\corollaryname}{Corollary}
\providecommand{\examplename}{Example}
\providecommand{\factname}{Fact}
\providecommand{\lemmaname}{Lemma}
\providecommand{\theoremname}{Theorem}

%TODO make these clickable
\newcommand{\Fref}[1]{Figure~\ref{fig:#1}}
\newcommand{\rulename}[1]{\ensuremath{\operatorname{#1}}}

\newcommand{\Blame}{\ensuremath{\textbf{Blame}}}
\newcommand{\blame}[3]{\ensuremath{#1\,\Blame{}_{#2,\,#3}}} % todo rename blame 3?
% as in \blame{a}{\ell}{o}

\newcommand{\Ch}[1]{Chapter #1} %TODO non breaking space
\newcommand{\ch}[1]{Chapter #1}


\newcommand{\ccnote}[1]{\todo[color=blue]{#1}} % responses to Chris's comments that I don't know that I want to completely change

\newcommand{\chp}{Chapter}
% TODO clickable link, chapter without number

% TODO also colon and spacing?
\newcommand{\tasys}{\vdash_{\mathrm{TAS}}}

% TODO delete?
\newcommand{\tasysr}{\vdash}

% constants that may need to be renamed/refonted...

% standardize use of terms
\newcommand{\Tit}{Type-in-type}
\newcommand{\tit}{type-in-type}
\newcommand{\bidir}{bidirectional}
\newcommand{\Bidir}{Bidirectional}
\newcommand{\cbv}{call-by-value}
\newcommand{\Cbv}{Call-by-value}
\newcommand{\CbV}{Call-by-Value} % for use in Headings
\newcommand{\whnf}{weak-head-normal-form}
\newcommand{\MartinL}{Martin-L{\"o}f}
\newcommand{\fullSp}{full spectrum}

% todo apply to prev chapters

% since spell check has issues with these
\newcommand{\scrut}{scrutinee}
\newcommand{\Scrut}{Scrutinee}
\newcommand{\scruts}{scrutinees}
\newcommand{\Sruts}{Scrutinees}

\newcommand{\slang}{surface language}
\newcommand{\Slang}{Surface language}
\newcommand{\SLang}{Surface Language} % for use in Headings
\newcommand{\clang}{cast language}
\newcommand{\Clang}{Cast language}
\newcommand{\CLang}{Cast Language}

\newcommand{\csys}{cast system}
\newcommand{\Csys}{Cast system}
\newcommand{\CSys}{Cast System} % for use in Headings

\newcommand{\case}{\ensuremath{\mathsf{case}}}

\newcommand{\maxRed}{\textbf{max}} % todo full replace

% standardize some fonts, captitalizarions
% also can take an optional number of params?
\newcommand{\Nat}{\ensuremath{\mathtt{Nat}}}

\newcommand{\Suc}{\ensuremath{\mathtt{S}}}

\newcommand{\Bool}{\ensuremath{\mathtt{Bool}}}

\newcommand{\True}{\ensuremath{\mathtt{True}}}
\newcommand{\False}{\ensuremath{\mathtt{False}}}

\newcommand{\Vect}{\ensuremath{\mathtt{Vec}}}
\newcommand{\Nil}{\ensuremath{\mathtt{Nil}}}
\newcommand{\Cons}{\ensuremath{\mathtt{Cons}}}

\newcommand{\Id}{\ensuremath{\mathtt{Id}}}
% \newcommand{\Refl}{\ensuremath{\mathtt{Refl}}}
% TODO could use texttt

% https://tex.stackexchange.com/questions/102483/subscript-and-superscript-in-lstlisting
\lstset{
  mathescape,         
  literate={=>}{$\Rightarrow$}{3}
           {->}{$\rightarrow$}{2}
}


% jargon
%TODO perhaps something that will handle capitalization and pluralization better?
% \newcommand{\slang}{surface language}
\acsetup{first-style=short}

\DeclareAcronym{TAS}{
  short=TAS,
  long=Type Assignment System
}
\DeclareAcronym{CC}{
  short=CC,
  long=Calculus of Constructions
}
\DeclareAcronym{ECC}{
  short=ECC,
  long=Extended Calculus of Constructions
}
\DeclareAcronym{ICC}{
  short=ICC,
  long=Implicit Calculus of Constructions
}
\DeclareAcronym{PTS}{
  short=PTS,
  long=Pure Type Systems
}
\DeclareAcronym{MLTT}{
  short=MLTT,
  long=Martin L{\"o}f Type Theory
}
\DeclareAcronym{ITT}{
  short=ITT,
  long=Intensional Type Theory % or intuitionistic?
}
\DeclareAcronym{ETT}{
  short=ETT,
  long=Extensional Type Theory
}
\DeclareAcronym{UTT}{
  short=UTT,
  long=Unified Type Theory
}
% TODO how should the acronym be capitalized
\DeclareAcronym{CIC}{
  short=CIC,
  long=Calculus of Inductive Constructions
}








% from https://tex.stackexchange.com/questions/277758/typesetting-a-calculus-grammar
% todo would need to figure out how to line up multiple grammars, and specify identifiers
\newenvironment{grammar}[2]
 {\begin{tabular}{@{\qquad}>{$}l<{$}@{\qquad}l@{}}
  \multicolumn{1}{@{}l@{}}{$#1$}&\multicolumn{1}{l@{}}{\hspace{-2em}#2}\\}
 {\end{tabular}}


 \renewcommand{\arraystretch}{1.2}
% TODO will probly need to do this on a case by case basis


%\usepackage{psfrag}
%\DeclareGraphicsExtensions{.eps}   % extension for included graphics
%\usepackage{thumbpdf}              % thumbnails for ps2pdf
%\usepackage[ps2pdf,                % hyper-references for ps2pdf
%bookmarks=true,%                   % generate bookmarks ...
%bookmarksnumbered=true,%           % ... with numbers
%hypertexnames=false,%              % needed for correct links to figures !!!
%breaklinks=true,%                  % breaks lines, but links are very small
%linkbordercolor={0 0 1},%          % blue frames around links
%pdfborder={0 0 112.0}]{hyperref}%  % border-width of frames 
%                                   % will be multiplied with 0.009 by ps2pdf
%\hypersetup{
%  pdfauthor   = {Joe Graduate <joe.graduate@bu.edu>},
%  pdftitle    = {dissertation.pdf},
%  pdfsubject  = {doctoral dissertations},
%  pdfkeywords = {mathematics, science, technology},
%  pdfcreator  = {LaTeX with hyperref package},
%  pdfproducer = {dvips + ps2pdf}
%}

% customized commands can be placed here
%\newcommand{\figref}[1]{Figure~\ref{#1}}
%\newcommand{\chapref}[1]{Chapter~\ref{#1}}
%\newcommand{\latex}{\LaTeX\xspace}