<!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 &gt;&gt; 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">
    &nbsp;
  </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>