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
|
<!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.test</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Library Coqdoc.test</h1>
<div class="code">
<span class="id" title="keyword">Class</span> <a id="C" class="idref" href="#C"><span class="id" title="record">C</span></a> := {}.<br/>
<br/>
<span class="id" title="keyword">Global Declare Instance</span> <a id="I0" class="idref" href="#I0"><span class="id" title="instance">I0</span></a> : <a class="idref" href="Coqdoc.test.html#C"><span class="id" title="class">C</span></a>.<br/>
<span class="id" title="keyword">Local Declare Instance</span> <a id="I1" class="idref" href="#I1"><span class="id" title="instance">I1</span></a> : <a class="idref" href="Coqdoc.test.html#C"><span class="id" title="class">C</span></a>.<br/>
<span class="id" title="keyword">Global Polymorphic Declare Instance</span> <a id="I3" class="idref" href="#I3"><span class="id" title="instance">I3</span></a> : <a class="idref" href="Coqdoc.test.html#C"><span class="id" title="class">C</span></a>.<br/>
<span class="id" title="keyword">Polymorphic Global Declare Instance</span> <a id="I4" class="idref" href="#I4"><span class="id" title="instance">I4</span></a> : <a class="idref" href="Coqdoc.test.html#C"><span class="id" title="class">C</span></a>.<br/>
<span class="id" title="keyword">Local Polymorphic Declare Instance</span> <a id="I5" class="idref" href="#I5"><span class="id" title="instance">I5</span></a> : <a class="idref" href="Coqdoc.test.html#C"><span class="id" title="class">C</span></a>.<br/>
<span class="id" title="keyword">Polymorphic Local Declare Instance</span> <a id="I6" class="idref" href="#I6"><span class="id" title="instance">I6</span></a> : <a class="idref" href="Coqdoc.test.html#C"><span class="id" title="class">C</span></a>.<br/>
<br/>
<span class="id" title="keyword">Global Program Instance</span> <a id="I7" class="idref" href="#I7"><span class="id" title="instance">I7</span></a> : <a class="idref" href="Coqdoc.test.html#C"><span class="id" title="class">C</span></a> := {}.<br/>
<span class="id" title="keyword">Local Program Instance</span> <a id="I8" class="idref" href="#I8"><span class="id" title="instance">I8</span></a> : <a class="idref" href="Coqdoc.test.html#C"><span class="id" title="class">C</span></a> := {}.<br/>
<span class="id" title="keyword">Program Global Instance</span> <a id="I9" class="idref" href="#I9"><span class="id" title="instance">I9</span></a> : <a class="idref" href="Coqdoc.test.html#C"><span class="id" title="class">C</span></a> := {}.<br/>
<span class="id" title="keyword">Program Local Instance</span> <a id="I10" class="idref" href="#I10"><span class="id" title="instance">I10</span></a> : <a class="idref" href="Coqdoc.test.html#C"><span class="id" title="class">C</span></a> := {}.<br/>
<br/>
<span class="id" title="keyword">Polymorphic Program Global Instance</span> <a id="I11" class="idref" href="#I11"><span class="id" title="instance">I11</span></a> : <a class="idref" href="Coqdoc.test.html#C"><span class="id" title="class">C</span></a> := {}.<br/>
<span class="id" title="keyword">Polymorphic Program Local Instance</span> <a id="I12" class="idref" href="#I12"><span class="id" title="instance">I12</span></a> : <a class="idref" href="Coqdoc.test.html#C"><span class="id" title="class">C</span></a> := {}.<br/>
<span class="id" title="keyword">Program Global Polymorphic Instance</span> <a id="I13" class="idref" href="#I13"><span class="id" title="instance">I13</span></a> : <a class="idref" href="Coqdoc.test.html#C"><span class="id" title="class">C</span></a> := {}.<br/>
<span class="id" title="keyword">Program Local Polymorphic Instance</span> <a id="I14" class="idref" href="#I14"><span class="id" title="instance">I14</span></a> : <a class="idref" href="Coqdoc.test.html#C"><span class="id" title="class">C</span></a> := {}.<br/>
<span class="id" title="keyword">Global Program Polymorphic Instance</span> <a id="I15" class="idref" href="#I15"><span class="id" title="instance">I15</span></a> : <a class="idref" href="Coqdoc.test.html#C"><span class="id" title="class">C</span></a> := {}.<br/>
<span class="id" title="keyword">Local Program Polymorphic Instance</span> <a id="I16" class="idref" href="#I16"><span class="id" title="instance">I16</span></a> : <a class="idref" href="Coqdoc.test.html#C"><span class="id" title="class">C</span></a> := {}.<br/>
<br/>
<span class="id" title="keyword">Global Notation</span> <a id="x0" class="idref" href="#x0"><span class="id" title="abbreviation">x0</span></a> := 0.<br/>
<span class="id" title="keyword">Local Notation</span> <a id="x1" class="idref" href="#x1"><span class="id" title="abbreviation">x1</span></a> := 0.<br/>
<br/>
<span class="id" title="keyword">Global Definition</span> <a id="x2" class="idref" href="#x2"><span class="id" title="definition">x2</span></a> := 0.<br/>
<span class="id" title="keyword">Local Definition</span> <a id="x3" class="idref" href="#x3"><span class="id" title="definition">x3</span></a> := 0.<br/>
<span class="id" title="keyword">Polymorphic Definition</span> <a id="x4" class="idref" href="#x4"><span class="id" title="definition">x4</span></a> := 0.<br/>
<span class="id" title="keyword">Polymorphic Global Definition</span> <a id="x5" class="idref" href="#x5"><span class="id" title="definition">x5</span></a> := 0.<br/>
<span class="id" title="keyword">Polymorphic Local Definition</span> <a id="x6" class="idref" href="#x6"><span class="id" title="definition">x6</span></a> := 0.<br/>
<span class="id" title="keyword">Global Polymorphic Definition</span> <a id="x7" class="idref" href="#x7"><span class="id" title="definition">x7</span></a> := 0.<br/>
<span class="id" title="keyword">Local Polymorphic Definition</span> <a id="x8" class="idref" href="#x8"><span class="id" title="definition">x8</span></a> := 0.<br/>
<br/>
<span class="id" title="keyword">Polymorphic Inductive</span> <a id="y0" class="idref" href="#y0"><span class="id" title="definition, inductive"><span id="y0_rect" class="id"><span id="y0_ind" class="id"><span id="y0_rec" class="id"><span id="y0_sind" class="id">y0</span></span></span></span></span></a> := <a id="z0" class="idref" href="#z0"><span class="id" title="constructor">z0</span></a>.<br/>
<span class="id" title="keyword">Polymorphic Variant</span> <a id="y1" class="idref" href="#y1"><span class="id" title="inductive">y1</span></a> := <a id="z1" class="idref" href="#z1"><span class="id" title="constructor">z1</span></a>.<br/>
<br/>
<span class="id" title="keyword">Local Obligation</span> <span class="id" title="keyword">Tactic</span> := <span class="id" title="tactic">auto</span>.<br/>
<span class="id" title="keyword">Global Obligation</span> <span class="id" title="keyword">Tactic</span> := <span class="id" title="tactic">auto</span>.<br/>
<br/>
<span class="id" title="keyword">Global Typeclasses Opaque</span> <span class="id" title="var">I7</span>.<br/>
<span class="id" title="keyword">Local Typeclasses Opaque</span> <span class="id" title="var">I8</span>.<br/>
<br/>
<span class="id" title="keyword">Global Hint Extern</span> 10 (<span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation">≤</span></a> <span class="id" title="var">_</span>) ⇒ <span class="id" title="tactic">auto</span> : <span class="id" title="var">arith</span>.<br/>
<span class="id" title="keyword">Local Hint Extern</span> 10 (<span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation">≤</span></a> <span class="id" title="var">_</span>) ⇒ <span class="id" title="tactic">auto</span> : <span class="id" title="var">arith</span>.<br/>
<br/>
<span class="id" title="keyword">Global Ltac</span> <span class="id" title="var">lt0</span> := <span class="id" title="tactic">auto</span>.<br/>
<span class="id" title="keyword">Local Ltac</span> <span class="id" title="var">lt1</span> := <span class="id" title="tactic">auto</span>.<br/>
<br/>
<span class="id" title="keyword">Require</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Program.Tactics.html#"><span class="id" title="library">Coq.Program.Tactics</span></a>.<br/>
<br/>
<span class="id" title="keyword">Global Program Definition</span> <a id="x9" class="idref" href="#x9"><span class="id" title="definition">x9</span></a> := 0.<br/>
<span class="id" title="keyword">Local Program Definition</span> <a id="x10" class="idref" href="#x10"><span class="id" title="definition">x10</span></a> := 0.<br/>
<span class="id" title="keyword">Program Global Definition</span> <a id="x11" class="idref" href="#x11"><span class="id" title="definition">x11</span></a> := 0.<br/>
<span class="id" title="keyword">Program Local Definition</span> <a id="x12" class="idref" href="#x12"><span class="id" title="definition">x12</span></a> := 0.<br/>
<br/>
<span class="id" title="keyword">Polymorphic Program Global Definition</span> <a id="x13" class="idref" href="#x13"><span class="id" title="definition">x13</span></a> := 0.<br/>
<span class="id" title="keyword">Polymorphic Program Local Definition</span> <a id="x14" class="idref" href="#x14"><span class="id" title="definition">x14</span></a> := 0.<br/>
<span class="id" title="keyword">Program Global Polymorphic Definition</span> <a id="x15" class="idref" href="#x15"><span class="id" title="definition">x15</span></a> := 0.<br/>
<span class="id" title="keyword">Program Local Polymorphic Definition</span> <a id="x16" class="idref" href="#x16"><span class="id" title="definition">x16</span></a> := 0.<br/>
<span class="id" title="keyword">Global Program Polymorphic Definition</span> <a id="x17" class="idref" href="#x17"><span class="id" title="definition">x17</span></a> := 0.<br/>
<span class="id" title="keyword">Local Program Polymorphic Definition</span> <a id="x18" class="idref" href="#x18"><span class="id" title="definition">x18</span></a> := 0.<br/>
</div>
</div>
<div id="footer">
<hr/><a href="indexpage.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>
</div>
</body>
</html>
|
