-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathDivConq.Rle.MapThrough.html
More file actions
88 lines (66 loc) · 13.7 KB
/
Copy pathDivConq.Rle.MapThrough.html
File metadata and controls
88 lines (66 loc) · 13.7 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
<!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.Rle.MapThrough</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Library DivConq.Rle.MapThrough</h1>
<div class="code">
</div>
<div class="doc">
<a id="lab28"></a><h1 class="section">MapThrough</h1>
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="DivConq.Dc.Dc.html#"><span class="id" title="library">Dc</span></a>.<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="DivConq.Dc.Dci.html#"><span class="id" title="library">Dci</span></a>.<br/>
<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/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="DivConq.Dc.Functors.html#"><span class="id" title="library">Functors</span></a>.<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="DivConq.List.List.html#"><span class="id" title="library">List.List</span></a>.<br/>
<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Lists.List.html#"><span class="id" title="library">Coq.Lists.List</span></a>.<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Nat.html#"><span class="id" title="library">Coq.Init.Nat</span></a>.<br/>
<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">ListNotations</span>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="mappedT" class="idref" href="#mappedT"><span class="id" title="definition">mappedT</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>) : <span class="id" title="keyword">Set</span> :=<br/>
<span class="id" title="keyword">∀</span>(<a id="R:3" class="idref" href="#R:3"><span class="id" title="binder">R</span></a> : <span class="id" title="keyword">Set</span>)(<a id="sfo:4" class="idref" href="#sfo:4"><span class="id" title="binder">sfo</span></a>:<a class="idref" href="DivConq.List.List.html#ListSFoldT"><span class="id" title="definition">ListSFoldT</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#A:1"><span class="id" title="variable">A</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#R:3"><span class="id" title="variable">R</span></a>),<br/>
<a class="idref" href="DivConq.Rle.MapThrough.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.Rle.MapThrough.html#R:3"><span class="id" title="variable">R</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.Rle.MapThrough.html#B:2"><span class="id" title="variable">B</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">×</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#R:3"><span class="id" title="variable">R</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a id="MapThrough" class="idref" href="#MapThrough"><span class="id" title="section">MapThrough</span></a>.<br/>
<br/>
<span class="id" title="keyword">Context</span> {<a id="A:5" class="idref" href="#A:5"><span class="id" title="binder">A</span></a> : <span class="id" title="keyword">Set</span>}.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="MapThroughAlg" class="idref" href="#MapThroughAlg"><span class="id" title="definition">MapThroughAlg</span></a>{<a id="B:6" class="idref" href="#B:6"><span class="id" title="binder">B</span></a> : <span class="id" title="keyword">Set</span>}(<a id="f:7" class="idref" href="#f:7"><span class="id" title="binder">f</span></a> : <a class="idref" href="DivConq.Rle.MapThrough.html#mappedT"><span class="id" title="definition">mappedT</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#MapThrough.A"><span class="id" title="variable">A</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#B:6"><span class="id" title="variable">B</span></a>) : <a class="idref" href="DivConq.List.List.html#ListAlg"><span class="id" title="definition">ListAlg</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#MapThrough.A"><span class="id" title="variable">A</span></a> (<a class="idref" href="DivConq.Dc.Functors.html#Const"><span class="id" title="definition">Const</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#B:6"><span class="id" title="variable">B</span></a>)) :=<br/>
<a class="idref" href="DivConq.Dc.Dc.html#rollAlg"><span class="id" title="definition">rollAlg</span></a> (<span class="id" title="keyword">fun</span> <a id="R:8" class="idref" href="#R:8"><span class="id" title="binder">R</span></a> <span class="id" title="var">_</span> <a id="sfo:9" class="idref" href="#sfo:9"><span class="id" title="binder">sfo</span></a> <a id="mapThrough:10" class="idref" href="#mapThrough:10"><span class="id" title="binder">mapThrough</span></a> <a id="xs:11" class="idref" href="#xs:11"><span class="id" title="binder">xs</span></a> ⇒ <br/>
<span class="id" title="keyword">match</span> <a class="idref" href="DivConq.Rle.MapThrough.html#xs:11"><span class="id" title="variable">xs</span></a> <span class="id" title="keyword">with</span><br/>
<a class="idref" href="DivConq.List.List.html#Nil"><span class="id" title="constructor">Nil</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a><br/>
| <a class="idref" href="DivConq.List.List.html#Cons"><span class="id" title="constructor">Cons</span></a> <span class="id" title="var">hd</span> <span class="id" title="var">tl</span> ⇒<br/>
<span class="id" title="keyword">let</span> (<a id="b:13" class="idref" href="#b:13"><span class="id" title="binder">b</span></a>,<a id="c:14" class="idref" href="#c:14"><span class="id" title="binder">c</span></a>) := <a class="idref" href="DivConq.Rle.MapThrough.html#f:7"><span class="id" title="variable">f</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#R:8"><span class="id" title="variable">R</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#sfo:9"><span class="id" title="variable">sfo</span></a> <span class="id" title="var">hd</span> <span class="id" title="var">tl</span> <span class="id" title="tactic">in</span><br/>
<a class="idref" href="DivConq.Rle.MapThrough.html#b:13"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#mapThrough:10"><span class="id" title="variable">mapThrough</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#c:14"><span class="id" title="variable">c</span></a><br/>
<span class="id" title="keyword">end</span>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="mapThroughr" class="idref" href="#mapThroughr"><span class="id" title="definition">mapThroughr</span></a>{<a id="R:15" class="idref" href="#R:15"><span class="id" title="binder">R</span></a> : <span class="id" title="keyword">Set</span>}(<a id="fo:16" class="idref" href="#fo:16"><span class="id" title="binder">fo</span></a> : <a class="idref" href="DivConq.List.List.html#ListFoldT"><span class="id" title="definition">ListFoldT</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#MapThrough.A"><span class="id" title="variable">A</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#R:15"><span class="id" title="variable">R</span></a>)<br/>
{<a id="B:17" class="idref" href="#B:17"><span class="id" title="binder">B</span></a> : <span class="id" title="keyword">Set</span>}(<a id="f:18" class="idref" href="#f:18"><span class="id" title="binder">f</span></a> : <a class="idref" href="DivConq.Rle.MapThrough.html#mappedT"><span class="id" title="definition">mappedT</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#MapThrough.A"><span class="id" title="variable">A</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#B:17"><span class="id" title="variable">B</span></a>) : <a class="idref" href="DivConq.Rle.MapThrough.html#R:15"><span class="id" title="variable">R</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.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#B:17"><span class="id" title="variable">B</span></a> :=<br/>
<a class="idref" href="DivConq.Rle.MapThrough.html#fo:16"><span class="id" title="variable">fo</span></a> (<a class="idref" href="DivConq.Dc.Functors.html#Const"><span class="id" title="definition">Const</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#B:17"><span class="id" title="variable">B</span></a>)) (<a class="idref" href="DivConq.Dc.Functors.html#FunConst"><span class="id" title="instance">FunConst</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#B:17"><span class="id" title="variable">B</span></a>)) (<a class="idref" href="DivConq.Rle.MapThrough.html#MapThroughAlg"><span class="id" title="definition">MapThroughAlg</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#f:18"><span class="id" title="variable">f</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="mapThrough" class="idref" href="#mapThrough"><span class="id" title="definition">mapThrough</span></a>{<a id="B:19" class="idref" href="#B:19"><span class="id" title="binder">B</span></a> : <span class="id" title="keyword">Set</span>}(<a id="f:20" class="idref" href="#f:20"><span class="id" title="binder">f</span></a> : <a class="idref" href="DivConq.Rle.MapThrough.html#mappedT"><span class="id" title="definition">mappedT</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#MapThrough.A"><span class="id" title="variable">A</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#B:19"><span class="id" title="variable">B</span></a>) : <a class="idref" href="DivConq.List.List.html#List"><span class="id" title="definition">List</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#MapThrough.A"><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="http://coq.inria.fr/distrib/V8.13.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#B:19"><span class="id" title="variable">B</span></a> :=<br/>
<a class="idref" href="DivConq.Rle.MapThrough.html#mapThroughr"><span class="id" title="definition">mapThroughr</span></a> (<a class="idref" href="DivConq.Dc.Dc.html#fold"><span class="id" title="definition">fold</span></a> (<a class="idref" href="DivConq.List.List.html#ListF"><span class="id" title="inductive">ListF</span></a> <a class="idref" href="DivConq.Rle.MapThrough.html#MapThrough.A"><span class="id" title="variable">A</span></a>)) <a class="idref" href="DivConq.Rle.MapThrough.html#f:20"><span class="id" title="variable">f</span></a>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="DivConq.Rle.MapThrough.html#MapThrough"><span class="id" title="section">MapThrough</span></a>.<br/>
<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>