agda-forester/macros.tree at main · samtoth/agda-forester · 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

\xmlns:html{http://www.w3.org/1999/xhtml}

\def\embed[src]{
  \<html:embed>[type]{text/html}[src]{\src}{}
}

\def\agda[bod]{
\<html:div>[class]{Agda}{
\pre{\bod}
}
}

\def\spanclass[col][bod]{\<html:span>[class]{\col}{\bod}}

\def\Function[bod]{\spanclass{Function}{\bod}}
\def\Symbol[bod]{\spanclass{Symbol}{\bod}}
\def\Generalizable[bod]{\bod}
\def\Bound[bod]{\bod}
\def\Keyword[bod]{\spanclass{Keyword}{\bod}}
\def\Primitive[bod]{\spanclass{Primitive}\bod}
\def\Comment[bod]{\spanclass{Comment}{\bod}}
\def\Postulate[bod]{\spanclass{Postulate}{\bod}}
\def\Operator[op]{\op}
\def\Module[bod]{\spanclass{Module}{\bod}}
\def\Pragma[bod]{\bod}
\def\Number[bod]{\spanclass{Number}{\bod}}
\def\Datatype[bod]{\spanclass{Datatype}{\bod}}
\def\Record[bod]{\spanclass{Record}{\bod}}
\def\InductiveConstructor[bod]{\spanclass{InductiveConstructor}{\bod}}
\def\Argument[bod]{\bod}
\def\DottedPattern[bod]{\bod}
\def\Field[bod]{\spanclass{Field}{\bod}}

\def\lpar[a]{\startverb(\stopverb}
\def\rpar[a]{\startverb)\stopverb}
\def\lbrace[a]{\startverb{\stopverb}
\def\rbrace[a]{\startverb}\stopverb}
\def\lbrack[a]{\startverb[\stopverb}
\def\rbrack[a]{\startverb]\stopverb}