-
Notifications
You must be signed in to change notification settings - Fork 0
/
handlers.fmt
94 lines (92 loc) · 2.44 KB
/
handlers.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
%if style == poly
%format (Forall (a)) = "\!"
%format (implicit(a)) = "\!"
%format (hidden(a)) = "\!"
%format (ldotsHere(a)) = "\ldots"
%format (hiddenConst (a)) = a
%format N = "\mathbb{N}"
%format e1 = e "_1"
%format e2 = e "_2"
%format v1 = v "_1"
%format v2 = v "_2"
%format x1 = x "_1"
%format x2 = x "_2"
%format t1 = t "_1"
%format t2 = t "_2"
%format s1 = s "_1"
%format s2 = s "_2"
%format c1 = c "_1"
%format c1, = c "_1,"
%format c2 = c "_2"
%format c2, = c "_2,"
%format f1 = f "_1"
%format f2 = f "_2"
%format g1 = g "_1"
%format g2 = g "_2"
%format i1 = i "_1"
%format i2 = i "_2"
%format nd1 = nd "_1"
%format nd2 = nd "_2"
%format pt1 = pt "_1"
%format pt2 = pt "_2"
%format law1 = law "_1"
%format law2 = law "_2"
%format law3 = law "_3"
%format law4 = law "_4"
%format top = "\top"
%format <-> = "\leftrightarrow"
%format refines = "\sqsubseteq"
%format subset = "\subseteq"
%format elem = "\in"
%format wpEval = wp "_{" eval "}"
%format wpCR = wp
%format _tril_ = "\_\triangleleft\_"
%format tril = "\triangleleft"
%format _trir_ = "\_\triangleright\_"
%format trir = "\triangleright"
%format maxPost' = maxPost
%format maxSpec' = maxSpec
%format if' = if
%format ^^ = "\;"
%format Set1 = Set
%format forall = "\forall"
%format _>>=_ = "\_\!\bind\!\_"
%format _>=>_ = "\_\!>\!\!\!\!\mathbin{=}\!\!\!\!>\!\_"
%format >=> = ">\!\!\!\!\mathbin{=}\!\!\!\!>"
%format constructor = "\Keyword{constructor}"
%format wpState' = wpState
%format statePT' = statePT
%format [[ = [
%format ]] = ]
%format [[_,_]] = [_,_]
%format correctnessAdd = correctness
%format correctnessProduct = correctness
%format correctnessRelabel = correctness
%format f91-partial-correctness = corectness
%format forall = "\forall"
%format Sigma = "\Sigma"
%format (seq (a) (b)) = "[" a "\ldots" a "+" b "]"
%format (instantiate (a)) = " " a " "
%format relabelSpec1 = relabelSpec "_1"
%format relabelSpec2 = relabelSpec "_2"
%format ~~> = "\looparrowright"
%format _~~>_ = "\_\looparrowright\_"
%format (SetOne) = "\Conid{Set}"
%format (SetL(l)) = "\Conid{Set}"
%else
%format (Forall (a)) = "forall { " a " } -> "
%format (implicit(a)) = "{" a "} ->"
%format (hidden(a)) = "{" a "}"
%format (instantiate (a)) = "(" a " {a})"
%format (hiddenConst (a)) = "(const " a ")"
%format (ldotsHere(a)) = a
%format N = "Nat"
%format top = "⊤"
%format ^^ = " "
%format _tril_ = _▹_
%format tril = ▹
%format _trir_ = _◃_
%format trir = ◃
%format (SetOne) = "(Set₁)"
%format (SetL(l)) = "(Set (" l "))"
%endif