JoeyEremondi · July 1, 2021 22:23
diff --git a/main.tex b/main.tex
 % !TeX root = main.tex
 % !TeX spellcheck = en-US
 %%% TeX-command-extra-options: "-shell-escape"

 %%
 %% This is file `sample-acmsmall.tex',
 %% generated with the docstrip utility.
 %%
 %% The original source files were:
 %%
 %% samples.dtx  (with options: `acmsmall')
 %%
 %% IMPORTANT NOTICE:
 %%
 %% For the copyright see the source file.
 %%
 %% Any modified versions of this file must be renamed
 %% with new filenames distinct from sample-acmsmall.tex.
 %%
 %% For distribution of the original source see the terms
 %% for copying and modification in the file samples.dtx.
 %%
 %% This generated file may be distributed as long as the
 %% original source files, as listed above, are part of the
 %% same distribution. (The sources need not necessarily be
 %% in the same archive or directory.)
 %%
 %% The first command in your LaTeX source must be the \documentclass command.
 \documentclass[autogobble,dvipsnames,acmsmall,review,anonymous]{acmart}

 \makeatletter


 % \def\@testdef #1#2#3{%
 % \def\reserved@a{#3}\expandafter \ifx \csname #1@#2\endcsname
 % \reserved@a  \else
 % \typeout{^^Jlabel #2 changed:^^J%
 % \meaning\reserved@a^^J%
 % \expandafter\meaning\csname #1@#2\endcsname^^J}%
 % \@tempswatrue \fi}


 \input{sharedmacros}
 \input{macros}



 %%
 %% \BibTeX command to typeset BibTeX logo in the docs
 \AtBeginDocument{%
  \providecommand\BibTeX{{%
    \normalfont B\kern-0.5em{\scshape i\kern-0.25em b}\kern-0.8em\TeX}}}

 %% Rights management information.  This information is sent to you
 %% when you complete the rights form.  These commands have SAMPLE
 %% values in them; it is your responsibility as an author to replace
 %% the commands and values with those provided to you when you
 %% complete the rights form.
 \setcopyright{acmcopyright}
 \copyrightyear{2018}
 \acmYear{2018}
 \acmDOI{10.1145/1122445.1122456}


 %%
 %% These commands are for a JOURNAL article.
 \acmJournal{JACM}
 \acmVolume{37}
 \acmNumber{4}
 \acmArticle{111}
 \acmMonth{8}

 %%
 %% Submission ID.
 %% Use this when submitting an article to a sponsored event. You'll
 %% receive a unique submission ID from the organizers
 %% of the event, and this ID should be used as the parameter to this command.
 %%\acmSubmissionID{123-A56-BU3}

 %%
 %% The majority of ACM publications use numbered citations and
 %% references.  The command \citestyle{authoryear} switches to the
 %% "author year" style.
 %%
 %% If you are preparing content for an event
 %% sponsored by ACM SIGGRAPH, you must use the "author year" style of
 %% citations and references.
 %% Uncommenting
 %% the next command will enable that style.
 \citestyle{acmauthoryear}


 %%
 %% end of the preamble, start of the body of the document source.
 \begin{document}

 \input{titleauthor}

 %%
 %% The "title" command has an optional parameter,
 %% allowing the author to define a "short title" to be used in page headers.

 %%
 %% The abstract is a short summary of the work to be presented in the
 %% article.
 \begin{abstract}
  \input{abstract}
 \end{abstract}

 %%
 %% The code below is generated by the tool at http://dl.acm.org/ccs.cfm.
 %% Please copy and paste the code instead of the example below.
 %%
 % \begin{CCSXML}
 % <ccs2012>
 %  <concept>
 %   <concept_id>10010520.10010553.10010562</concept_id>
 %   <concept_desc>Computer systems organization~Embedded systems</concept_desc>
 %   <concept_significance>500</concept_significance>
 %  </concept>
 %  <concept>
 %   <concept_id>10010520.10010575.10010755</concept_id>
 %   <concept_desc>Computer systems organization~Redundancy</concept_desc>
 %   <concept_significance>300</concept_significance>
 %  </concept>
 %  <concept>
 %   <concept_id>10010520.10010553.10010554</concept_id>
 %   <concept_desc>Computer systems organization~Robotics</concept_desc>
 %   <concept_significance>100</concept_significance>
 %  </concept>
 %  <concept>
 %   <concept_id>10003033.10003083.10003095</concept_id>
 %   <concept_desc>Networks~Network reliability</concept_desc>
 %   <concept_significance>100</concept_significance>
 %  </concept>
 % </ccs2012>
 % \end{CCSXML}

 \ccsdesc[500]{Theory of computation~Type structures}
 \ccsdesc[500]{Theory of computation~Program semantics}

 %%
 %% Keywords. The author(s) should pick words that accurately describe
 %% the work being presented. Separate the keywords with commas.
 \keywords{dependent types, gradual types, inductive families, propositional equality}


 %%
 %% This command processes the author and affiliation and title
 %% information and builds the first part of the formatted document.
 \maketitle

 \input{content}

 \bibliographystyle{ACM-Reference-Format}
 \bibliography{myRefs}


 \appendix
 \input{apx-proofs}

 \end{document}
 \endinput
 %%
 %% End of file `sample-acmsmall.tex'.
	% !TeX root = main.tex
	% !TeX spellcheck = en-US
	%%% TeX-command-extra-options: "-shell-escape"

	%%
	%% This is file `sample-acmsmall.tex',
	%% generated with the docstrip utility.
	%%
	%% The original source files were:
	%%
	%% samples.dtx (with options: `acmsmall')
	%%
	%% IMPORTANT NOTICE:
	%%
	%% For the copyright see the source file.
	%%
	%% Any modified versions of this file must be renamed
	%% with new filenames distinct from sample-acmsmall.tex.
	%%
	%% For distribution of the original source see the terms
	%% for copying and modification in the file samples.dtx.
	%%
	%% This generated file may be distributed as long as the
	%% original source files, as listed above, are part of the
	%% same distribution. (The sources need not necessarily be
	%% in the same archive or directory.)
	%%
	%% The first command in your LaTeX source must be the \documentclass command.
	\documentclass[autogobble,dvipsnames,acmsmall,review,anonymous]{acmart}

	\makeatletter


	% \def\@testdef #1#2#3{%
	% \def\reserved@a{#3}\expandafter \ifx \csname #1@#2\endcsname
	% \reserved@a \else
	% \typeout{^^Jlabel #2 changed:^^J%
	% \meaning\reserved@a^^J%
	% \expandafter\meaning\csname #1@#2\endcsname^^J}%
	% \@tempswatrue \fi}


	\input{sharedmacros}
	\input{macros}



	%%
	%% \BibTeX command to typeset BibTeX logo in the docs
	\AtBeginDocument{%
	\providecommand\BibTeX{{%
	\normalfont B\kern-0.5em{\scshape i\kern-0.25em b}\kern-0.8em\TeX}}}

	%% Rights management information. This information is sent to you
	%% when you complete the rights form. These commands have SAMPLE
	%% values in them; it is your responsibility as an author to replace
	%% the commands and values with those provided to you when you
	%% complete the rights form.
	\setcopyright{acmcopyright}
	\copyrightyear{2018}
	\acmYear{2018}
	\acmDOI{10.1145/1122445.1122456}


	%%
	%% These commands are for a JOURNAL article.
	\acmJournal{JACM}
	\acmVolume{37}
	\acmNumber{4}
	\acmArticle{111}
	\acmMonth{8}

	%%
	%% Submission ID.
	%% Use this when submitting an article to a sponsored event. You'll
	%% receive a unique submission ID from the organizers
	%% of the event, and this ID should be used as the parameter to this command.
	%%\acmSubmissionID{123-A56-BU3}

	%%
	%% The majority of ACM publications use numbered citations and
	%% references. The command \citestyle{authoryear} switches to the
	%% "author year" style.
	%%
	%% If you are preparing content for an event
	%% sponsored by ACM SIGGRAPH, you must use the "author year" style of
	%% citations and references.
	%% Uncommenting
	%% the next command will enable that style.
	\citestyle{acmauthoryear}


	%%
	%% end of the preamble, start of the body of the document source.
	\begin{document}

	\input{titleauthor}

	%%
	%% The "title" command has an optional parameter,
	%% allowing the author to define a "short title" to be used in page headers.

	%%
	%% The abstract is a short summary of the work to be presented in the
	%% article.
	\begin{abstract}
	\input{abstract}
	\end{abstract}

	%%
	%% The code below is generated by the tool at http://dl.acm.org/ccs.cfm.
	%% Please copy and paste the code instead of the example below.
	%%
	% \begin{CCSXML}
	% <ccs2012>
	% <concept>
	% <concept_id>10010520.10010553.10010562</concept_id>
	% <concept_desc>Computer systems organization~Embedded systems</concept_desc>
	% <concept_significance>500</concept_significance>
	% </concept>
	% <concept>
	% <concept_id>10010520.10010575.10010755</concept_id>
	% <concept_desc>Computer systems organization~Redundancy</concept_desc>
	% <concept_significance>300</concept_significance>
	% </concept>
	% <concept>
	% <concept_id>10010520.10010553.10010554</concept_id>
	% <concept_desc>Computer systems organization~Robotics</concept_desc>
	% <concept_significance>100</concept_significance>
	% </concept>
	% <concept>
	% <concept_id>10003033.10003083.10003095</concept_id>
	% <concept_desc>Networks~Network reliability</concept_desc>
	% <concept_significance>100</concept_significance>
	% </concept>
	% </ccs2012>
	% \end{CCSXML}

	\ccsdesc[500]{Theory of computation~Type structures}
	\ccsdesc[500]{Theory of computation~Program semantics}

	%%
	%% Keywords. The author(s) should pick words that accurately describe
	%% the work being presented. Separate the keywords with commas.
	\keywords{dependent types, gradual types, inductive families, propositional equality}


	%%
	%% This command processes the author and affiliation and title
	%% information and builds the first part of the formatted document.
	\maketitle

	\input{content}

	\bibliographystyle{ACM-Reference-Format}
	\bibliography{myRefs}


	\appendix
	\input{apx-proofs}

	\end{document}
	\endinput
	%%
	%% End of file `sample-acmsmall.tex'.