-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathDivConq.Dc.Functors.html
More file actions
124 lines (97 loc) · 27 KB
/
Copy pathDivConq.Dc.Functors.html
File metadata and controls
124 lines (97 loc) · 27 KB
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
115
116
117
118
119
120
121
122
123
124
<!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>DivConq.Dc.Functors</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Library DivConq.Dc.Functors</h1>
<div class="code">
</div>
<div class="doc">
<a id="lab3"></a><h1 class="section">Functors</h1>
The Functors file includes a fair amount of generic definitions we reuse
elsewhere (such as the <span class="inlinecode"><a class="idref" href="DivConq.Dc.Functors.html#Functor"><span class="id" title="record">Functor</span></a></span> typeclass). We also store some frequently used
functors, e.g., <span class="inlinecode"><a class="idref" href="DivConq.Dc.Functors.html#Const"><span class="id" title="definition">Const</span></a></span> and <span class="inlinecode"><a class="idref" href="DivConq.Dc.Functors.html#Id"><span class="id" title="definition">Id</span></a></span>.
</div>
<div class="code">
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="DivConq.Dc.Kinds.html#"><span class="id" title="library">Kinds</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="FmapT" class="idref" href="#FmapT"><span class="id" title="definition">FmapT</span></a>(<a id="A:1" class="idref" href="#A:1"><span class="id" title="binder">A</span></a> <a id="B:2" class="idref" href="#B:2"><span class="id" title="binder">B</span></a> : <span class="id" title="keyword">Set</span>)(<a id="F:3" class="idref" href="#F:3"><span class="id" title="binder">F</span></a> : <span class="id" title="keyword">Set</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Set</span>) : <span class="id" title="keyword">Set</span> := <span class="id" title="keyword">∀</span>(<a id="f:4" class="idref" href="#f:4"><span class="id" title="binder">f</span></a> : <a class="idref" href="DivConq.Dc.Functors.html#A:1"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="DivConq.Dc.Functors.html#B:2"><span class="id" title="variable">B</span></a>), <a class="idref" href="DivConq.Dc.Functors.html#F:3"><span class="id" title="variable">F</span></a> <a class="idref" href="DivConq.Dc.Functors.html#A:1"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="DivConq.Dc.Functors.html#F:3"><span class="id" title="variable">F</span></a> <a class="idref" href="DivConq.Dc.Functors.html#B:2"><span class="id" title="variable">B</span></a>.<br/>
<span class="id" title="keyword">Definition</span> <a id="FmapId" class="idref" href="#FmapId"><span class="id" title="definition">FmapId</span></a>(<a id="F:5" class="idref" href="#F:5"><span class="id" title="binder">F</span></a> : <span class="id" title="keyword">Set</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Set</span>)(<a id="fmap:8" class="idref" href="#fmap:8"><span class="id" title="binder">fmap</span></a> : <span class="id" title="keyword">∀</span>{<a id="A:6" class="idref" href="#A:6"><span class="id" title="binder">A</span></a> <a id="B:7" class="idref" href="#B:7"><span class="id" title="binder">B</span></a> : <span class="id" title="keyword">Set</span>}, <a class="idref" href="DivConq.Dc.Functors.html#FmapT"><span class="id" title="definition">FmapT</span></a> <a class="idref" href="DivConq.Dc.Functors.html#A:6"><span class="id" title="variable">A</span></a> <a class="idref" href="DivConq.Dc.Functors.html#B:7"><span class="id" title="variable">B</span></a> <a class="idref" href="DivConq.Dc.Functors.html#F:5"><span class="id" title="variable">F</span></a>) : <span class="id" title="keyword">Set</span> :=<br/>
<span class="id" title="keyword">∀</span> (<a id="A:9" class="idref" href="#A:9"><span class="id" title="binder">A</span></a> : <span class="id" title="keyword">Set</span>) (<a id="x:10" class="idref" href="#x:10"><span class="id" title="binder">x</span></a> : <a class="idref" href="DivConq.Dc.Functors.html#F:5"><span class="id" title="variable">F</span></a> <a class="idref" href="DivConq.Dc.Functors.html#A:9"><span class="id" title="variable">A</span></a>), <a class="idref" href="DivConq.Dc.Functors.html#fmap:8"><span class="id" title="variable">fmap</span></a> (<span class="id" title="keyword">fun</span> <a id="x:11" class="idref" href="#x:11"><span class="id" title="binder">x</span></a> ⇒ <a class="idref" href="DivConq.Dc.Functors.html#x:11"><span class="id" title="variable">x</span></a>) <a class="idref" href="DivConq.Dc.Functors.html#x:10"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="DivConq.Dc.Functors.html#x:10"><span class="id" title="variable">x</span></a> .<br/>
<br/>
<span class="id" title="keyword">Class</span> <a id="Functor" class="idref" href="#Functor"><span class="id" title="record">Functor</span></a> (<a id="F:12" class="idref" href="#F:12"><span class="id" title="binder">F</span></a> : <span class="id" title="keyword">Set</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Set</span>) :=<br/>
{<br/>
<a id="fmap" class="idref" href="#fmap"><span class="id" title="projection">fmap</span></a> : <span class="id" title="keyword">∀</span> {<a id="A:14" class="idref" href="#A:14"><span class="id" title="binder">A</span></a> <a id="B:15" class="idref" href="#B:15"><span class="id" title="binder">B</span></a> : <span class="id" title="keyword">Set</span>}, <a class="idref" href="DivConq.Dc.Functors.html#FmapT"><span class="id" title="definition">FmapT</span></a> <a class="idref" href="DivConq.Dc.Functors.html#A:14"><span class="id" title="variable">A</span></a> <a class="idref" href="DivConq.Dc.Functors.html#B:15"><span class="id" title="variable">B</span></a> <a class="idref" href="DivConq.Dc.Functors.html#F:12"><span class="id" title="variable">F</span></a>;<br/>
<a id="fmapId" class="idref" href="#fmapId"><span class="id" title="projection">fmapId</span></a> : <a class="idref" href="DivConq.Dc.Functors.html#FmapId"><span class="id" title="definition">FmapId</span></a> <a class="idref" href="DivConq.Dc.Functors.html#F:12"><span class="id" title="variable">F</span></a> (@<a class="idref" href="DivConq.Dc.Functors.html#fmap:16"><span class="id" title="method">fmap</span></a>)<br/>
}.<br/>
<br/>
</div>
<div class="doc">
Identity, option, and constant <span class="inlinecode"><span class="id" title="var">functor</span></span>s.
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a id="Id" class="idref" href="#Id"><span class="id" title="definition">Id</span></a>(<a id="X:18" class="idref" href="#X:18"><span class="id" title="binder">X</span></a>:<span class="id" title="keyword">Set</span>) : <span class="id" title="keyword">Set</span> := <a class="idref" href="DivConq.Dc.Functors.html#X:18"><span class="id" title="variable">X</span></a>.<br/>
<span class="id" title="keyword">Global Instance</span> <a id="FunId" class="idref" href="#FunId"><span class="id" title="instance">FunId</span></a> : <a class="idref" href="DivConq.Dc.Functors.html#Functor"><span class="id" title="class">Functor</span></a> <a class="idref" href="DivConq.Dc.Functors.html#Id"><span class="id" title="definition">Id</span></a> := {<br/>
<a class="idref" href="DivConq.Dc.Functors.html#fmap"><span class="id" title="method">fmap</span></a> := <span class="id" title="keyword">fun</span> <a id="A:19" class="idref" href="#A:19"><span class="id" title="binder">A</span></a> <a id="B:20" class="idref" href="#B:20"><span class="id" title="binder">B</span></a> <a id="c:21" class="idref" href="#c:21"><span class="id" title="binder">c</span></a> <a id="xs:22" class="idref" href="#xs:22"><span class="id" title="binder">xs</span></a> ⇒ <a class="idref" href="DivConq.Dc.Functors.html#c:21"><span class="id" title="variable">c</span></a> <a class="idref" href="DivConq.Dc.Functors.html#xs:22"><span class="id" title="variable">xs</span></a> ; <a class="idref" href="DivConq.Dc.Functors.html#fmapId"><span class="id" title="method">fmapId</span></a> := <span class="id" title="keyword">fun</span> <a id="A:23" class="idref" href="#A:23"><span class="id" title="binder">A</span></a> <a id="x:24" class="idref" href="#x:24"><span class="id" title="binder">x</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Logic.html#eq_refl"><span class="id" title="constructor">eq_refl</span></a><br/>
}.<br/>
<br/>
<span class="id" title="keyword">Global Instance</span> <a id="FunOption" class="idref" href="#FunOption"><span class="id" title="instance">FunOption</span></a> : <a class="idref" href="DivConq.Dc.Functors.html#Functor"><span class="id" title="class">Functor</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> :=<br/>
{ <a class="idref" href="DivConq.Dc.Functors.html#fmap"><span class="id" title="method">fmap</span></a> := <span class="id" title="keyword">fun</span> <a id="A:25" class="idref" href="#A:25"><span class="id" title="binder">A</span></a> <a id="B:26" class="idref" href="#B:26"><span class="id" title="binder">B</span></a> <a id="c:27" class="idref" href="#c:27"><span class="id" title="binder">c</span></a> <a id="o:28" class="idref" href="#o:28"><span class="id" title="binder">o</span></a> ⇒ <span class="id" title="keyword">match</span> <a class="idref" href="DivConq.Dc.Functors.html#o:28"><span class="id" title="variable">o</span></a> <span class="id" title="keyword">with</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">x</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> (<a class="idref" href="DivConq.Dc.Functors.html#c:27"><span class="id" title="variable">c</span></a> <span class="id" title="var">x</span>) | <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> <span class="id" title="keyword">end</span>;<br/>
<a class="idref" href="DivConq.Dc.Functors.html#fmapId"><span class="id" title="method">fmapId</span></a> := <span class="id" title="keyword">fun</span> <a id="A:30" class="idref" href="#A:30"><span class="id" title="binder">A</span></a> <a id="o:31" class="idref" href="#o:31"><span class="id" title="binder">o</span></a> ⇒ <span class="id" title="keyword">match</span> <a class="idref" href="DivConq.Dc.Functors.html#o:31"><span class="id" title="variable">o</span></a> <span class="id" title="keyword">with</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">x</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Logic.html#eq_refl"><span class="id" title="constructor">eq_refl</span></a> | <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Logic.html#eq_refl"><span class="id" title="constructor">eq_refl</span></a> <span class="id" title="keyword">end</span> }.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="Const" class="idref" href="#Const"><span class="id" title="definition">Const</span></a>(<a id="T:33" class="idref" href="#T:33"><span class="id" title="binder">T</span></a>: <span class="id" title="keyword">Set</span>) : <span class="id" title="keyword">Set</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Set</span> := <span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> ⇒ <a class="idref" href="DivConq.Dc.Functors.html#T:33"><span class="id" title="variable">T</span></a>.<br/>
<span class="id" title="keyword">Global Instance</span> <a id="FunConst" class="idref" href="#FunConst"><span class="id" title="instance">FunConst</span></a>(<a id="T:34" class="idref" href="#T:34"><span class="id" title="binder">T</span></a> : <span class="id" title="keyword">Set</span>) : <a class="idref" href="DivConq.Dc.Functors.html#Functor"><span class="id" title="class">Functor</span></a> (<a class="idref" href="DivConq.Dc.Functors.html#Const"><span class="id" title="definition">Const</span></a> <a class="idref" href="DivConq.Dc.Functors.html#T:34"><span class="id" title="variable">T</span></a>) :=<br/>
{<a class="idref" href="DivConq.Dc.Functors.html#fmap"><span class="id" title="method">fmap</span></a> := <span class="id" title="keyword">fun</span> <a id="A:35" class="idref" href="#A:35"><span class="id" title="binder">A</span></a> <a id="B:36" class="idref" href="#B:36"><span class="id" title="binder">B</span></a> <a id="f:37" class="idref" href="#f:37"><span class="id" title="binder">f</span></a> <a id="xs:38" class="idref" href="#xs:38"><span class="id" title="binder">xs</span></a> ⇒ <a class="idref" href="DivConq.Dc.Functors.html#xs:38"><span class="id" title="variable">xs</span></a>;<br/>
<a class="idref" href="DivConq.Dc.Functors.html#fmapId"><span class="id" title="method">fmapId</span></a> := <span class="id" title="keyword">fun</span> <a id="A:39" class="idref" href="#A:39"><span class="id" title="binder">A</span></a> <a id="xs:40" class="idref" href="#xs:40"><span class="id" title="binder">xs</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Logic.html#eq_refl"><span class="id" title="constructor">eq_refl</span></a> }.<br/>
<br/>
</div>
<div class="doc">
Indexed (dependent) versions.
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Section</span> <a id="Ind" class="idref" href="#Ind"><span class="id" title="section">Ind</span></a>.<br/>
<span class="id" title="keyword">Variable</span> <a id="Ind.I" class="idref" href="#Ind.I"><span class="id" title="variable">I</span></a> : <span class="id" title="keyword">Set</span>.<br/>
<span class="id" title="keyword">Definition</span> <a id="kMo" class="idref" href="#kMo"><span class="id" title="definition">kMo</span></a> := <a class="idref" href="DivConq.Dc.Kinds.html#kMo"><span class="id" title="definition">kMo</span></a> <a class="idref" href="DivConq.Dc.Functors.html#Ind.I"><span class="id" title="variable">I</span></a> .<br/>
<br/>
<span class="id" title="keyword">Section</span> <a id="Ind.IndF" class="idref" href="#Ind.IndF"><span class="id" title="section">IndF</span></a>.<br/>
<span class="id" title="keyword">Variable</span> <a id="Ind.IndF.Fi" class="idref" href="#Ind.IndF.Fi"><span class="id" title="variable">Fi</span></a> : <a class="idref" href="DivConq.Dc.Functors.html#kMo"><span class="id" title="definition">kMo</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="DivConq.Dc.Functors.html#kMo"><span class="id" title="definition">kMo</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="FmapiT" class="idref" href="#FmapiT"><span class="id" title="definition">FmapiT</span></a>(<a id="A:43" class="idref" href="#A:43"><span class="id" title="binder">A</span></a> <a id="B:44" class="idref" href="#B:44"><span class="id" title="binder">B</span></a> : <a class="idref" href="DivConq.Dc.Functors.html#kMo"><span class="id" title="definition">kMo</span></a>) : <span class="id" title="keyword">Set</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <a id="i:45" class="idref" href="#i:45"><span class="id" title="binder">i</span></a> : <a class="idref" href="DivConq.Dc.Functors.html#Ind.I"><span class="id" title="variable">I</span></a>, <a class="idref" href="DivConq.Dc.Functors.html#A:43"><span class="id" title="variable">A</span></a> <a class="idref" href="DivConq.Dc.Functors.html#i:45"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="DivConq.Dc.Functors.html#B:44"><span class="id" title="variable">B</span></a> <a class="idref" href="DivConq.Dc.Functors.html#i:45"><span class="id" title="variable">i</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">∀</span> <a id="i:46" class="idref" href="#i:46"><span class="id" title="binder">i</span></a> : <a class="idref" href="DivConq.Dc.Functors.html#Ind.I"><span class="id" title="variable">I</span></a> , <a class="idref" href="DivConq.Dc.Functors.html#Ind.IndF.Fi"><span class="id" title="variable">Fi</span></a> <a class="idref" href="DivConq.Dc.Functors.html#A:43"><span class="id" title="variable">A</span></a> <a class="idref" href="DivConq.Dc.Functors.html#i:46"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="DivConq.Dc.Functors.html#Ind.IndF.Fi"><span class="id" title="variable">Fi</span></a> <a class="idref" href="DivConq.Dc.Functors.html#B:44"><span class="id" title="variable">B</span></a> <a class="idref" href="DivConq.Dc.Functors.html#i:46"><span class="id" title="variable">i</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="FmapiId" class="idref" href="#FmapiId"><span class="id" title="definition">FmapiId</span></a>(<a id="fmapi:49" class="idref" href="#fmapi:49"><span class="id" title="binder">fmapi</span></a> : <span class="id" title="keyword">∀</span>{<a id="A:47" class="idref" href="#A:47"><span class="id" title="binder">A</span></a> <a id="B:48" class="idref" href="#B:48"><span class="id" title="binder">B</span></a> : <a class="idref" href="DivConq.Dc.Functors.html#kMo"><span class="id" title="definition">kMo</span></a>}, <a class="idref" href="DivConq.Dc.Functors.html#FmapiT"><span class="id" title="definition">FmapiT</span></a> <a class="idref" href="DivConq.Dc.Functors.html#A:47"><span class="id" title="variable">A</span></a> <a class="idref" href="DivConq.Dc.Functors.html#B:48"><span class="id" title="variable">B</span></a>) : <span class="id" title="keyword">Set</span> :=<br/>
<span class="id" title="keyword">∀</span> (<a id="A:50" class="idref" href="#A:50"><span class="id" title="binder">A</span></a> : <a class="idref" href="DivConq.Dc.Functors.html#kMo"><span class="id" title="definition">kMo</span></a>) (<a id="i:51" class="idref" href="#i:51"><span class="id" title="binder">i</span></a> : <a class="idref" href="DivConq.Dc.Functors.html#Ind.I"><span class="id" title="variable">I</span></a>)(<a id="x:52" class="idref" href="#x:52"><span class="id" title="binder">x</span></a> : <a class="idref" href="DivConq.Dc.Functors.html#Ind.IndF.Fi"><span class="id" title="variable">Fi</span></a> <a class="idref" href="DivConq.Dc.Functors.html#A:50"><span class="id" title="variable">A</span></a> <a class="idref" href="DivConq.Dc.Functors.html#i:51"><span class="id" title="variable">i</span></a>), <a class="idref" href="DivConq.Dc.Functors.html#fmapi:49"><span class="id" title="variable">fmapi</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> <a id="x:53" class="idref" href="#x:53"><span class="id" title="binder">x</span></a> ⇒ <a class="idref" href="DivConq.Dc.Functors.html#x:53"><span class="id" title="variable">x</span></a>) <a class="idref" href="DivConq.Dc.Functors.html#i:51"><span class="id" title="variable">i</span></a> <a class="idref" href="DivConq.Dc.Functors.html#x:52"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="DivConq.Dc.Functors.html#x:52"><span class="id" title="variable">x</span></a> .<br/>
<br/>
<span class="id" title="keyword">Class</span> <a id="Functori" class="idref" href="#Functori"><span class="id" title="record">Functori</span></a> :=<br/>
{<br/>
<a id="fmapi" class="idref" href="#fmapi"><span class="id" title="projection">fmapi</span></a> : <span class="id" title="keyword">∀</span> {<a id="A:55" class="idref" href="#A:55"><span class="id" title="binder">A</span></a> <a id="B:56" class="idref" href="#B:56"><span class="id" title="binder">B</span></a> : <a class="idref" href="DivConq.Dc.Functors.html#kMo"><span class="id" title="definition">kMo</span></a>}, <a class="idref" href="DivConq.Dc.Functors.html#FmapiT"><span class="id" title="definition">FmapiT</span></a> <a class="idref" href="DivConq.Dc.Functors.html#A:55"><span class="id" title="variable">A</span></a> <a class="idref" href="DivConq.Dc.Functors.html#B:56"><span class="id" title="variable">B</span></a>;<br/>
<a id="fmapiId" class="idref" href="#fmapiId"><span class="id" title="projection">fmapiId</span></a> : <a class="idref" href="DivConq.Dc.Functors.html#FmapiId"><span class="id" title="definition">FmapiId</span></a> (@<a class="idref" href="DivConq.Dc.Functors.html#fmapi:57"><span class="id" title="method">fmapi</span></a>)<br/>
}.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="DivConq.Dc.Functors.html#Ind.IndF"><span class="id" title="section">IndF</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="Consti" class="idref" href="#Consti"><span class="id" title="definition">Consti</span></a>(<a id="R:59" class="idref" href="#R:59"><span class="id" title="binder">R</span></a>: <a class="idref" href="DivConq.Dc.Functors.html#kMo"><span class="id" title="definition">kMo</span></a>) : <a class="idref" href="DivConq.Dc.Functors.html#kMo"><span class="id" title="definition">kMo</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="DivConq.Dc.Functors.html#kMo"><span class="id" title="definition">kMo</span></a> := <span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> <a id="d:60" class="idref" href="#d:60"><span class="id" title="binder">d</span></a> ⇒ <a class="idref" href="DivConq.Dc.Functors.html#R:59"><span class="id" title="variable">R</span></a> <a class="idref" href="DivConq.Dc.Functors.html#d:60"><span class="id" title="variable">d</span></a>.<br/>
<span class="id" title="keyword">Global Instance</span> <a id="FunConsti" class="idref" href="#FunConsti"><span class="id" title="instance">FunConsti</span></a>(<a id="R:61" class="idref" href="#R:61"><span class="id" title="binder">R</span></a> : <a class="idref" href="DivConq.Dc.Functors.html#kMo"><span class="id" title="definition">kMo</span></a>) : <a class="idref" href="DivConq.Dc.Functors.html#Functori"><span class="id" title="class">Functori</span></a> (<a class="idref" href="DivConq.Dc.Functors.html#Consti"><span class="id" title="definition">Consti</span></a> <a class="idref" href="DivConq.Dc.Functors.html#R:61"><span class="id" title="variable">R</span></a>) :=<br/>
{ <a class="idref" href="DivConq.Dc.Functors.html#fmapi"><span class="id" title="method">fmapi</span></a> := <span class="id" title="keyword">fun</span> <a id="A:62" class="idref" href="#A:62"><span class="id" title="binder">A</span></a> <a id="B:63" class="idref" href="#B:63"><span class="id" title="binder">B</span></a> <a id="f:64" class="idref" href="#f:64"><span class="id" title="binder">f</span></a> <a id="i:65" class="idref" href="#i:65"><span class="id" title="binder">i</span></a> <a id="xs:66" class="idref" href="#xs:66"><span class="id" title="binder">xs</span></a> ⇒ <a class="idref" href="DivConq.Dc.Functors.html#xs:66"><span class="id" title="variable">xs</span></a>;<br/>
<a class="idref" href="DivConq.Dc.Functors.html#fmapiId"><span class="id" title="method">fmapiId</span></a> := <span class="id" title="keyword">fun</span> <a id="A:67" class="idref" href="#A:67"><span class="id" title="binder">A</span></a> <a id="x:68" class="idref" href="#x:68"><span class="id" title="binder">x</span></a> <a id="c:69" class="idref" href="#c:69"><span class="id" title="binder">c</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Logic.html#eq_refl"><span class="id" title="constructor">eq_refl</span></a> }.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="DivConq.Dc.Functors.html#Ind"><span class="id" title="section">Ind</span></a>.<br/>
<br/>
<span class="id" title="var">Arguments</span> <a class="idref" href="DivConq.Dc.Functors.html#Consti"><span class="id" title="definition">Consti</span></a>{<span class="id" title="var">I</span>}.<br/>
<span class="id" title="var">Arguments</span> <a class="idref" href="DivConq.Dc.Functors.html#FunConsti"><span class="id" title="instance">FunConsti</span></a>{<span class="id" title="var">I</span>}.<br/>
</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>