-
Notifications
You must be signed in to change notification settings - Fork 0
/
terms.tex
115 lines (99 loc) · 4.34 KB
/
terms.tex
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
\RequirePackage{amsmath,xparse,xpatch,xspace,xstring,listofitems}
%%% MACROS FOR TYPESETTING MMT TERMS %%%
\providecommand{\cn}[1]{\ensuremath{\mathtt{#1}}}
% e.g., \makecn{neut} makes the typeset name of a constant "neut" available as under a new TeX macro \neut.
% If you want the macro name to differ, pass another one as the optional argument, e.g.
% \makecn[neutconst]{neut} would make "neut" being typeset by a new macro \neutconst.
% star the command to force overwrite previous commands (e.g., built-in in latex or other packages)
\NewDocumentCommand\makecn{somO{\cn}}{%
\IfBooleanTF{#1}{
\IfValueTF{#2}{%
\expandafter\def\csname#2\endcsname{#4{#3}\xspace}%
}{%
\expandafter\def\csname#3\endcsname{#4{#3}\xspace}%
}%
}{%
\IfValueTF{#2}{%
\expandafter\NewDocumentCommand\csname#2\endcsname{}{#4{#3}\xspace}%
}{%
\expandafter\NewDocumentCommand\csname#3\endcsname{}{#4{#3}\xspace}%
}%
}%
}
% GENERAL
% ==================================================
\newcommand\denseTo{\kern -0.15em\to\kern -0.15em}
% Command \myDots (renamed to \denseLdots here) copied and adapted from <https://tex.stackexchange.com/a/200849>
% User: LaRiFaRi <https://tex.stackexchange.com/users/32245/larifari>
% License: CC BY-SA 3.0 <https://creativecommons.org/licenses/by-sa/3.0/>
\newcommand{\denseLdots}{\ifmmode\mathinner{\kern-0.06em\ldotp\kern-0.2em\ldotp\kern-0.2em\ldotp\kern-0.06em}\else.\kern-0.13em.\kern-0.13em.\fi}
% \quantifier{q}{x} typesets `q x.\ `
% \quantifier{q}{x}[T] typesets `q x: T.\ `
% \quantifier{q}{x y} typesets `q x y.\ `
% \quantifier{q}{x y}[T] typesets `q x y: T.\ `
%
% see \lam, \tpi, \lampi
%
% If you want to use macros as bound variable names, be sure to end them via {} or some super/subscript, e.g.
% with `\newcommand\hatx{\hat{x}}
% instead of `\quantifier{q}{\hatx \hatx^y \hatx_z}` you have to write `\quantifier{q}{\hatx{} \hatx^y \hatx_z}`
% holds for all derived macros, too (esp. \lam, \tpi, ...)
\NewDocumentCommand\quantifier{m m o}{%
#1
\setsepchar{ }\readlist\vars{#2}% read list of arguments separated by space
\foreachitem\var\in\vars{\var\;}\mspace{-5mu}% print out all arguments separated by \;, and undoing the trailing \; by an mspace
\IfValueT{#3}{\colon #3}%
.\ %
}
% Typesets flexary quantifier usage.
% Examples:
% - `Q x1 ... xn.`
% use `\flexQuantifier{Q}{x1}{xn}`
% - `Q x1 ... xn: a.`
% use `\flexQuantifier{Q}{x1}{xn}[a]`
% - `Q x1: a1. ... Q xn: an.`
% use `\flexQuantifier{Q}{x1}[a1]{xn}[an]
\NewDocumentCommand\flexQuantifier{m mo mo}{%
\IfValueTF{#3}{%
\quantifier{#1}{#2}[#3]\,\denseLdots\,\quantifier{#1}{#4}[#5]%
}{%
\quantifier{#1}{#2 \denseLdots #4}[#5]%
}
}
% (partially copied from frmacros, Florian Rabe's personal collection of LaTeX macros)
\newcommand{\mmt}{\texorpdfstring{{\normalfont\scshape{Mmt}}\xspace}{MMT\ }}
\newcommand{\omdoc}{{\scshape{OMDoc}}\xspace}
\newcommand{\omdocmmt}{{\scshape{OMDoc}}/\mmt}
\newcommand{\mmtlf}{\texorpdfstring{{\normalfont\scshape{Mmt}/LF}\xspace}{MMT/LF\ }}
\newcommand{\ommt}{\omdocmmt}
\newcommand{\mathml}{{\scshape{MathML}}\xspace}
\newcommand{\openmath}{{\scshape{OpenMath}}\xspace}
\newcommand{\keyword}[1]{\operatorname{\mathbf{#1}}}
\newcommand{\mor}{\ensuremath{\rightsquigarrow}}
\newcommand{\includedIn}{\ensuremath{\hookrightarrow}}
\newcommand{\including}{\ensuremath{\hookleftarrow}}
\newcommand{\id}[1]{\mathrm{id}_{#1}}
% ==================================================
% LF
% ==================================================
\input{terms-lf}
% ==================================================
% UNTYPED TERMS
% ==================================================
\makecn{term}
% ==================================================
% HARD-TYPED TERMS
% ==================================================
\makecn*{tp}
\makecn[tmc]{tm}
\NewDocumentCommand\tm{m}{\tmc\ #1}
\NewDocumentCommand\tmSymbol{}{\tmc} % deprecated alias of \tmc
% ==================================================
% SOFT-TYPED TERMS
% ==================================================
\newcommand{\ofTermType}[2]{#1\mathrel{::}#2}
% ==================================================
% LOGIC (PL, FOL, SFOL, and more)
% ==================================================
\input{terms-logic}
% ==================================================