/
lambdapi.tex
44 lines (43 loc) · 1.3 KB
/
lambdapi.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
\definecolor{lightgrey}{RGB}{240,240,240}
\lstdefinelanguage{Lambdapi}
{
inputencoding=utf8,
extendedchars=true,
numbers=none,
numberstyle={},
tabsize=2,
basicstyle={\ttfamily\small\upshape},
backgroundcolor=\color{lightgrey},
keywords={abort,admit,admitted,apply,as,assert,assertnot,associative,assume,begin,builtin,commutative,compute,constant,debug,end,fail,flag,focus,generalize,have,in,induction,inductive,infix,injective,left,let,notation,off,on,opaque,open,prefix,print,private,proofterm,protected,prover,prover_timeout,quantifier,refine,reflexivity,require,rewrite,right,rule,sequential,simplify,solve,symbol,symmetry,type,TYPE,unif_rule,verbose,why3,with},
sensitive=true,
keywordstyle=\color{blue},
morecomment=[l]{//},
morecomment=[n]{/*}{*/},
commentstyle={\itshape\color{red}},
string=[b]{"},
stringstyle=\color{orange},
showstringspaces=false,
literate=
{λ}{$\lambda$}1
{↪}{$\hookrightarrow$}1
{→}{$\rightarrow$}1
{Π}{$\Pi$}1
{≔}{$\coloneqq$}1
{⊢}{$\vdash$}1
{≡}{$\equiv$}1
{𝔹}{$\mathbb{B}$}1
{𝕃}{$\mathbb{L}$}1
{ℕ}{$\mathbb{N}$}1
{α}{$\alpha$}1
{β}{$\beta$}1
{η}{$\eta$}1
{π}{$\pi$}1
{τ}{$\tau$}1
{ω}{$\omega$}1
{∧}{$\wedge$}1
{≤}{$\le$}1
{≠}{$\neq$}1
{∉}{$\notin$}1
{×}{$\times$}1
{⋅}{$\cdot$}1
}