-
Notifications
You must be signed in to change notification settings - Fork 24
/
Copy pathmine.fmt
executable file
·112 lines (76 loc) · 2.34 KB
/
mine.fmt
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
%% Misc lhs2TeX directives
%format Unit = " \mathbf{1} "
%% %format Unit = " \mathbbm{1} "
%format :* = " \times "
%format :+ = " + "
%% %format <> = " \mathbin{\oplus} "
%% %format `mappend` = " \mathbin{\oplus} "
%format <> = " \diamond "
%format `mappend` = " \diamond "
%format mempty = epsilon
%% %format <> = " \mathbin{<>} "
%format <$> = "\mathbin{<\!\!\!\$\!\!\!>}"
% Got from Andres L:
\newcommand{\calculationcomments}{%
\let\onelinecomment=\onelinecommentchars
\def\commentbegin{\quad\{ }%
\def\commentend{\}}%
}
\calculationcomments
%format NOTHING = "{}"
%% hack: add missing space, e.g., before "{" in data type decl
%format SPACE = "\ {}"
%format PAUSE = "\pause "
%format BACK = "{\Back}"
%format BACKQ a = "{\Back}"
%format PBACK = "\pause\Back"
% \renewcommand{\onelinecomment}{\it}
%% %format (meaning (a)) = "\db{" a "}"
%% %format meaning' (a) x = "\db{" a "}" x
%format meaning = mu
%format meaning' = mu
%format meaningInv = mu "^{-1}"
%% %format Meaning = "\Mu"
%% %format meaning = "\mu"
%% %format Lin1 = Lin "_1"
%% %format idL = "\Varid{id_L}"
%format idL = "\widehat{" id "}"
%format @. = "\mathbin{\hat{\circ}}"
%format @* = "\mathbin{\times}"
%format NO = "{}"
%format -* = "\multimap"
%format :-* = "\mathbin{:"-*"}"
%% %format :-* = "\mathbin{\mathtt{:\!\!-\!*}}"
%format Lin = "(":-*")"
%format :&& = "\mathbin{:\!"&&&"}"
%format :|| = "\mathbin{:\!"|||"}"
%format *** = "\mathbin{\times}"
%format &&& = "\mathbin{\smalltriangleup}"
%format ||| = "\mathbin{\smalltriangledown}"
%% %format *** = "\symThree{*}"
%% %format &&& = "\symThree{\&}"
%% %format ||| = "\symThree{|}"
%format Prod k a b = a "\times_{" k "}" b
%format Coprod k a b = a "+_{" k "}" b
%% %format T = "{\cal T}"
%% %format T = "{\cal R}"
%% %format T = "\mathbb{T}"
%format R = "\mathbb{R}"
%format R2 = "\mathbb{R}^2"
%format <$> = "\mathbin{<\!\!\!\$\!\!\!>}"
%format <*> = "\mathbin{<\!\!\!*\!\!\!>}"
%format :->: = "\twoheadrightarrow"
%format <== = "\Leftarrow"
%format liftA2 = "\Varid{liftA\!_2}"
%format liftA3 = "\Varid{liftA\!_3}"
%format liftA4 = "\Varid{liftA\!_4}"
%format lift0 = "\Varid{lift_0}"
%format lift1 = "\Varid{lift_1}"
%format lift2 = "\Varid{lift_2}"
%format lift3 = "\Varid{lift_3}"
%format lift4 = "\Varid{lift_4}"
%format ==> = "\Longrightarrow"
%format :. = "\circ"
%% %format lub = "\sqcup"
%format ta = "t_a"
%format b0