<!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">co
q</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://rocq-prover.org/">coqdoc</a>
</div>
</div>
</body>
</html>
