termcomp-reference/main.tex at main · TermCOMP/termcomp-reference · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
\documentclass{report}

\usepackage{amsthm}
\usepackage[colorlinks=true]{hyperref}
\usepackage{amssymb}
\usepackage{mathtools}
\usepackage{microtype}
\usepackage{stmaryrd}
\usepackage[most]{tcolorbox}
\usepackage[dvipsnames]{xcolor}
\usepackage{cleveref}
\usepackage{enumitem}
\usepackage{nicefrac}

\theoremstyle{theorem}\newtheorem{theorem}{Theorem}
\theoremstyle{definition}\newtheorem{example}[theorem]{Example}

\newcommand{\CC}{\mathcal{C}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\B}{\mathbb{B}}
\newcommand{\F}{\mathcal{F}}
\newcommand{\V}{\mathcal{V}}
\newcommand{\Sorts}{\mathcal{S}}
\newcommand{\Types}{\mathcal{T}\!ypes}
\newcommand{\Rules}{\mathcal{R}}
\newcommand{\FV}{\mathit{FV}}

\newcommand{\domain}{\mathtt{domain}}

\newcommand{\asort}{\iota}
\newcommand{\atype}{\sigma}
\newcommand{\btype}{\tau}
\newcommand{\identifier}[1]{\mathtt{#1}}
\newcommand{\afun}{\identifier{f}}
\newcommand{\avar}{x}
\newcommand{\bvar}{y}
\newcommand{\cvar}{z}

\newcommand{\hastype}{\ \mathtt{::}\ }

\newcommand{\abs}[3]{\lambda #1\!:\!#2.#3}
\newcommand{\app}[2]{#1 \cdot #2}
\newcommand{\apps}[3]{#1 \cdot #2 \cdots #3}
\newcommand{\metaabs}[2]{\langle #1\rangle#2}
\newcommand{\metaabsn}[4]{\metaabs{#1_1\!:\!#2_1,\dots,#1_n\!:\!#2_{#3}}{#4}}
\newcommand{\metaabslist}[3]{\langle #1_1\!:\!#2_1,\dots,#1_n\!:\!#2_{#3} \rangle}

\newcommand{\arity}{\mathit{ar}}
\newcommand{\arrtype}{\rightarrow}
\newcommand{\arrz}{\Rightarrow}
\newcommand{\arr}[1]{\arrz_{#1}}
\newcommand{\supterm}{\rhd}
\newcommand{\suptermeq}{\unrhd}
\newcommand{\replace}[3]{#1_{#2:=#3}}

\newcommand{\symb}[1]{\mathtt{#1}}

\newcommand{\nul}{\symb{0}}
\newcommand{\nil}{\symb{nil}}
\newcommand{\cons}{\symb{cons}}
\newcommand{\suc}{\symb{s}}
\newcommand{\map}{\symb{map}}

\newcommand{\nat}{\symb{nat}}

\newcommand{\guard}[1]{\llbracket #1 \rrbracket}
\DeclareMathOperator{\rc}{rc}
\DeclareMathOperator{\dheight}{dh}

\renewcommand{\comment}[1]{\footnote{!!! #1}}

\usepackage{amsthm}
\newtheorem{definition}{Definition}

%TRS
\newcommand{\ito}{\mathrel{\smash{\stackrel{\raisebox{2pt}{$\scriptscriptstyle \mathbf{i}\:$}}{\smash{\rightarrow}}}}}
\newcommand{\oto}{\mathrel{\smash{\stackrel{\raisebox{2pt}{$\scriptscriptstyle \mathbf{o}\:$}}{\smash{\rightarrow}}}}}

\makeatletter
\newcommand{\chapterauthor}[1]{%
  {\parindent0pt\vspace*{-25pt}%
  \linespread{1.1}\large\scshape#1%
  \par\nobreak\vspace*{35pt}}
  \@afterheading%
}
\renewenvironment{abstract}{%
  \par\small
  \begin{quote}
  \noindent\textbf{Abstract.}~
}{%
  \end{quote}
  \normalsize
}
\newenvironment{formalproblem}[4]{%
  \begin{tcolorbox}[
    enhanced,
    breakable,
    colback=ForestGreen!2!white,
    colframe=ForestGreen!45!black,
    colbacktitle=ForestGreen!18!white,
    coltitle=black,
    boxrule=0.6pt,
    arc=2mm,
    left=1.5mm,
    right=1.5mm,
    top=1.2mm,
    bottom=1.2mm,
    title={#1},
    fonttitle=\bfseries,
    separator sign none
  ]
  \textbf{Input:} #2

  \smallskip
  \textbf{Question:} #3

  \smallskip
  \textbf{Possible Outputs:} #4
}{%
  \end{tcolorbox}
}

\newenvironment{grammar}[1]{%
  \begin{tcolorbox}[
    enhanced,
    breakable,
    colback=RoyalBlue!2!white,
    colframe=RoyalBlue!45!black,
    colbacktitle=RoyalBlue!18!white,
    coltitle=black,
    boxrule=0.6pt,
    arc=2mm,
    left=1.5mm,
    right=1.5mm,
    top=1.2mm,
    bottom=1.2mm,
    title={#1},
    fonttitle=\bfseries,
    separator sign none
  ]
}{%
  \end{tcolorbox}
}
\makeatother

\title{The termCOMP Reference}

\begin{document}

\maketitle

\tableofcontents
\input{general}
\input{trs}
\input{srs}
\input{ptrs}
\input{stcrs}
\input{its}
\input{c}
\input{lp}

\bibliographystyle{plain}
\bibliography{stcrs}

\end{document}