blob: 070f80e7718430b157e9df6795ce077326600a3f (
plain)
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
|
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<title>Coqdoc.verbatim</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Library Coqdoc.verbatim</h1>
<div class="code">
</div>
<div class="doc">
<div class="paragraph"> </div>
<pre>
uint32_t shift_right( uint32_t a, uint32_t shift )
{
return a >> shift;
}
</pre>
<div class="paragraph"> </div>
This line and the following shows <code>verbatim </code> text:
<div class="paragraph"> </div>
<code> A stand-alone inline verbatim </code>
<div class="paragraph"> </div>
<code> A non-ended inline verbatim to test line location
</code>
<div class="paragraph"> </div>
<ul class="doclist">
<li> item 1
</li>
<li> item 2 is <code>verbatim</code>
</li>
<li> item 3 is <code>verbatim</code> too
<br/>
<span class="inlinecode"><span class="id" title="var">A</span> <span class="id" title="var">coq</span> <span class="id" title="var">block</span> : <span class="id" title="keyword">∀</span> <span class="id" title="var">n</span>, <span class="id" title="var">n</span> = 0
<div class="paragraph"> </div>
</span>
</li>
<li> <code>verbatim</code> again, and a formula <span class="inlinecode"></span> <span class="inlinecode"><span class="id" title="var">True</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">False</span></span> <span class="inlinecode"></span>
</li>
<li>
<pre>
multiline
verbatim
</pre>
</li>
<li> last item
</li>
</ul>
<div class="paragraph"> </div>
<center><table class="infrule">
<tr class="infruleassumption">
<td class="infrule">Γ ⊢ A</td>
<td class="infrulenamecol" rowspan="3">
</td></tr>
<tr class="infrulemiddle">
<td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
<td class="infrule">Γ ⊢ A ∨ B</td>
<td></td>
</tr>
</table></center>
<div class="paragraph"> </div>
<pre>
A non-ended block verbatim to test line location
*)
</pre>
</div>
<div class="code">
</div>
</div>
<div id="footer">
<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>
</div>
</body>
</html>
|
