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
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
|
<!DOCTYPE html>
<html lang="en">
<head id="htmx-head">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">
<meta name="description" content="Rocq Standard Library">
<meta name="twitter:title" content="Rocq Standard Library">
<meta name="twitter:description" content="Rocq Standard Library">
<meta name="twitter:image" content="https://rocq-prover.org/img/social/rocq-prover_org_social_media.png">
<meta property="og:site_name" content="Rocq">
<meta property="og:type" content="object">
<meta property="og:title" content="Rocq Standard Library">
<meta property="og:description" content="Rocq Standard Library">
<meta name="og:image" content="https://rocq-prover.org/img/social/rocq-prover_org_social_media.png">
<meta name="theme-color" content="#fff">
<meta name="color-scheme" content="white">
<meta name="ahrefs-site-verification" content="6ff715b377cdcd566334b44ae8888791189ce24640c8a403eacdc3bcbaa9449b">
<link rel="canonical" href="https://rocq-prover.org/doc">
<link rel="icon" type="image/x-icon" href="https://rocq-prover.org/logos/favicon_stdlib.ico">
<link rel="manifest" href="https://rocq-prover.org/manifest.json">
<link rel="stylesheet" href="https://rocq-prover.org/vendors/font-files/instrument-rocq.css">
<link rel="stylesheet" href="https://rocq-prover.org/vendors/font-files/source-code-pro.css">
<script defer="" src="https://rocq-prover.org/vendors/alpine-clipboard.js"></script>
<script defer="" src="https://rocq-prover.org/vendors/alpine.min.js"></script>
<script defer="" src="https://rocq-prover.org/vendors/htmx.min.js"></script>
<script defer="" data-domain="rocq-prover.org" src="https://rocq-prover.org/vendors/script.js"></script>
<link type="text/css" rel="stylesheet" media="all" href="https://rocq-prover.org/css/stdlib.css">
<link rel="search" href="http://rocq-prover.org/opensearch.xml" type="application/opensearchdescription+xml" title="Rocq">
<title>Rocq Standard Library</title>
<style>
.htmx-indicator {
opacity: 0;
transition: opacity 200ms ease-in;
}
.htmx-request .htmx-indicator {
opacity: 1
}
.htmx-request.htmx-indicator {
opacity: 1
}
</style>
</head>
<body style="overscroll-behavior-x: auto;">
<script>
if (localStorage.theme === 'dark' || (!('theme' in localStorage) && window.matchMedia && window.matchMedia('(prefers-color-scheme: dark)').matches)) {
document.body.classList.add("dark");
} else {
document.body.classList.remove("dark");
}
</script>
<header class="fixed top-0 z-50 w-full h-20 flex items-center flex-wrap" x-data="{ open: false }">
<nav class="bg-background container-fluid dark:bg-dark-background_navigation flex gap-5 h-20 header items-center justify-between rounded-b-lg shadow-sm wide xl:gap-8">
<ul class="order-0 space space-x-5 xl:space-x-8 items-center flex text-content font-medium dark:text-title dark:text-opacity-60 dark:font-semibold">
<li style="width:170px">
<a href="http://rocq-prover.org/" class="block">
<img src="https://rocq-prover.org/logos/logo-rocq-stdlib.svg" width="170" alt="Rocq stdlib logo" class="dark:hidden">
<img src="https://rocq-prover.org/logos/logo-rocq-stdlib-dark.svg" width="170" alt="Rocq stdlib logo" class="hidden dark:inline">
</a>
</li>
</ul>
<ul class="order-1 mr-auto items-center hidden lg:flex font-medium dark:text-white dark:text-opacity-60 dark:font-semibold">
<li><a href="http://rocq-prover.org/docs" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primary text-title dark:text-dark-title">Learn</a>
</li>
<li><a href="http://rocq-prover.org/platform" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primary text-primary dark:text-dark-primary">Platform</a>
</li>
<li><a href="http://rocq-prover.org/packages" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primary text-title dark:text-dark-title">Packages</a>
</li>
<li><a href="http://rocq-prover.org/community" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primary text-title dark:text-dark-title">Community</a>
</li>
<li><a href="http://rocq-prover.org/consortium" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primary text-title dark:text-dark-title">Consortium</a>
</li>
<li><a href="http://rocq-prover.org/changelog" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primary text-title dark:text-dark-title">News</a>
</li>
</ul>
<ul class="order-1 lg:hidden flex items-center">
<li class="h-12 w-12 hover:bg-tertiary_25 dark:hover:bg-primary_20 flex items-center justify-center rounded-full text-content dark:text-dark-title">
<button aria-label="open menu" @click="open = ! open">
<svg xmlns="http://www.w3.org/2000/svg" class="h-8 w-8" fill="none" viewBox="0 0 24 24" stroke="currentColor" aria-hidden="true">
<path stroke-linecap="round" stroke-linejoin="round" stroke-width="2" d="M4 6h16M4 12h16M4 18h16"></path>
</svg>
</button>
</li>
</ul>
</nav>
<div class="bg-black fixed w-full h-full left-0 top-0 opacity-60 z-40" x-show="open" style="display: none;"></div>
<nav class="z-50 h-full fixed right-0 top-0 max-w-full w-96 bg-background dark:bg-dark-background shadow-lg" x-show="open" @click.away="open = false" x-transition:enter="transition duration-200 ease-out" x-transition:enter-start="translate-x-full" x-transition:leave="transition duration-100 ease-in" x-transition:leave-end="translate-x-full" style="display: none;">
<ul class="text-content p-6 font-semibold">
<li class="flex justify-between items-center">
<a href="http://rocq-prover.org/">
<img src="https://rocq-prover.org/logos/logo-rocq-blue_orange.svg" width="132" alt="Rocq logo" class="dark:hidden">
<img src="https://rocq-prover.org/logos/logo-rocq-white.svg" width="132" alt="Rocq logo" class="hidden dark:inline">
</a>
<div class="" x-on:click="open = false">
<button aria-label="close" class="text-content dark:text-dark-title">
<svg xmlns="http://www.w3.org/2000/svg" class="h-8 w-8" fill="none" viewBox="0 0 24 24" stroke="currentColor" aria-hidden="true">
<path stroke-linecap="round" stroke-linejoin="round" stroke-width="2" d="M6 18L18 6M6 6l12 12"></path>
</svg>
</button>
</div>
</li>
<li><a href="http://rocq-prover.org/docs" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primaryblock text-title dark:text-dark-title">Learn</a>
</li>
<li><a href="http://rocq-prover.org/platform" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primaryblock text-primary dark:text-dark-primary">Platform</a>
</li>
<li><a href="http://rocq-prover.org/packages" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primaryblock text-title dark:text-dark-title">Packages</a>
</li>
<li><a href="http://rocq-prover.org/community" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primaryblock text-title dark:text-dark-title">Community</a>
</li>
<li><a href="http://rocq-prover.org/consortium" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primaryblock text-title dark:text-dark-title">Consortium</a>
</li>
<li><a href="http://rocq-prover.org/changelog" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primaryblock text-title dark:text-dark-title">News</a></li>
<li class="mt-3 mb-6">
<a href="http://rocq-prover.org/docs#beginner_section" class="w-full rounded font-normal py-3 px-7 flex items-center justify-center bg-primary dark:bg-dark-primary text-white dark:text-dark-title">Get started</a>
</li>
<li>
<div class="space-x-6 text-2xl flex items-center">
<a aria-label="Rocq's Zulip" href="https://coq.zulipchat.com/" class="opacity-60 hover:opacity-100 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">
<svg viewBox="0 0 256 256" version="1.1" class="w-6 h-6" fill="currentColor" aria-hidden="true" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" preserveAspectRatio="xMidYMid">
<path d="M128,0 C198.692448,0 256,57.307552 256,128 C256,198.692448 198.692448,256 128,256 C57.307552,256 0,198.692448 0,128 C0,57.307552 57.307552,0 128,0 Z M121.679533,118.222163 L75.7877336,159.200897 C71.0603547,162.920702 67.9584879,169.060511 67.9584879,175.967416 C67.9584879,187.245548 76.232162,196.475047 86.3444303,196.475047 L172.590938,196.475047 C182.703207,196.475047 190.976881,187.245548 190.976881,175.967416 C190.976881,164.68624 182.703207,155.459784 172.590938,155.459784 L107.299534,155.459784 C106.331533,155.459784 105.719683,154.300009 106.191507,153.356359 L123.024994,119.652857 C123.639888,118.669635 122.531861,117.491595 121.679533,118.222163 Z M172.590938,59.3627915 L86.3444303,59.3627915 C76.232162,59.3627915 67.9584879,68.58925 67.9584879,79.870426 C67.9584879,91.1485579 76.232162,100.378058 86.3444303,100.378058 L86.3444303,100.378058 L151.635834,100.378058 C152.603836,100.378058 153.215686,101.537833 152.743861,102.481482 L152.743861,102.481482 L135.910374,136.184985 C135.29548,137.168207 136.403507,138.346246 137.255836,137.615679 L137.255836,137.615679 L183.147635,96.6308563 C187.875014,92.9080074 190.976881,86.7712425 190.976881,79.8643379 C190.976881,68.586206 182.703207,59.3567064 172.590938,59.3627915 L172.590938,59.3627915 Z" fill="inherit"></path>
</svg>
</a>
<a aria-label="Rocq's Discourse" href="https://coq.discourse.group/" class="opacity-60 hover:opacity-100 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">
<svg xmlns="http://www.w3.org/2000/svg" class="w-6 h-6" fill="currentColor" viewBox="0 0 448 512" aria-hidden="true">
<path d="M225.9 32C103.3 32 0 130.5 0 252.1 0 256 .1 480 .1 480l225.8-.2c122.7 0 222.1-102.3 222.1-223.9C448 134.3 348.6 32 225.9 32zM224 384c-19.4 0-37.9-4.3-54.4-12.1L88.5 392l22.9-75c-9.8-18.1-15.4-38.9-15.4-61 0-70.7 57.3-128 128-128s128 57.3 128 128-57.3 128-128 128z"></path>
</svg>
</a>
<a aria-label="The Rocq Prover on GitHub" href="https://github.com/coq/coq" class="opacity-60 hover:opacity-100 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">
<svg xmlns="http://www.w3.org/2000/svg" class="w-6 h-6" fill="currentColor" viewBox="0 0 24 24" aria-hidden="true">
<path fill-rule="evenodd" d="M12 2C6.477 2 2 6.484 2 12.017c0 4.425 2.865 8.18 6.839 9.504.5.092.682-.217.682-.483 0-.237-.008-.868-.013-1.703-2.782.605-3.369-1.343-3.369-1.343-.454-1.158-1.11-1.466-1.11-1.466-.908-.62.069-.608.069-.608 1.003.07 1.531 1.032 1.531 1.032.892 1.53 2.341 1.088 2.91.832.092-.647.35-1.088.636-1.338-2.22-.253-4.555-1.113-4.555-4.951 0-1.093.39-1.988 1.029-2.688-.103-.253-.446-1.272.098-2.65 0 0 .84-.27 2.75 1.026A9.564 9.564 0 0112 6.844c.85.004 1.705.115 2.504.337 1.909-1.296 2.747-1.027 2.747-1.027.546 1.379.202 2.398.1 2.651.64.7 1.028 1.595 1.028 2.688 0 3.848-2.339 4.695-4.566 4.943.359.309.678.92.678 1.855 0 1.338-.012 2.419-.012 2.747 0 .268.18.58.688.482A10.019 10.019 0 0022 12.017C22 6.484 17.522 2 12 2z" clip-rule="evenodd"></path>
</svg>
</a>
<a aria-label="The Rocq Prover on Mastodon" rel="me" href="https://mastodon.acm.org/@RocqProver" class="opacity-60 hover:opacity-100 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">
<svg viewBox="0 0 74 79" class="w-6 h-6" fill="currentColor" xmlns="http://www.w3.org/2000/svg" aria-hidden="true">
<path d="M73.7014 17.4323C72.5616 9.05152 65.1774 2.4469 56.424 1.1671C54.9472 0.950843 49.3518 0.163818 36.3901 0.163818H36.2933C23.3281 0.163818 20.5465 0.950843 19.0697 1.1671C10.56 2.41145 2.78877 8.34604 0.903306 16.826C-0.00357854 21.0022 -0.100361 25.6322 0.068112 29.8793C0.308275 35.9699 0.354874 42.0498 0.91406 48.1156C1.30064 52.1448 1.97502 56.1419 2.93215 60.0769C4.72441 67.3445 11.9795 73.3925 19.0876 75.86C26.6979 78.4332 34.8821 78.8603 42.724 77.0937C43.5866 76.8952 44.4398 76.6647 45.2833 76.4024C47.1867 75.8033 49.4199 75.1332 51.0616 73.9562C51.0841 73.9397 51.1026 73.9184 51.1156 73.8938C51.1286 73.8693 51.1359 73.8421 51.1368 73.8144V67.9366C51.1364 67.9107 51.1302 67.8852 51.1186 67.862C51.1069 67.8388 51.0902 67.8184 51.0695 67.8025C51.0489 67.7865 51.0249 67.7753 50.9994 67.7696C50.9738 67.764 50.9473 67.7641 50.9218 67.7699C45.8976 68.9569 40.7491 69.5519 35.5836 69.5425C26.694 69.5425 24.3031 65.3699 23.6184 63.6327C23.0681 62.1314 22.7186 60.5654 22.5789 58.9744C22.5775 58.9477 22.5825 58.921 22.5934 58.8965C22.6043 58.8721 22.621 58.8505 22.6419 58.8336C22.6629 58.8167 22.6876 58.8049 22.714 58.7992C22.7404 58.7934 22.7678 58.794 22.794 58.8007C27.7345 59.9796 32.799 60.5746 37.8813 60.5733C39.1036 60.5733 40.3223 60.5733 41.5447 60.5414C46.6562 60.3996 52.0437 60.1408 57.0728 59.1694C57.1983 59.1446 57.3237 59.1233 57.4313 59.0914C65.3638 57.5847 72.9128 52.8555 73.6799 40.8799C73.7086 40.4084 73.7803 35.9415 73.7803 35.4523C73.7839 33.7896 74.3216 23.6576 73.7014 17.4323ZM61.4925 47.3144H53.1514V27.107C53.1514 22.8528 51.3591 20.6832 47.7136 20.6832C43.7061 20.6832 41.6988 23.2499 41.6988 28.3194V39.3803H33.4078V28.3194C33.4078 23.2499 31.3969 20.6832 27.3894 20.6832C23.7654 20.6832 21.9552 22.8528 21.9516 27.107V47.3144H13.6176V26.4937C13.6176 22.2395 14.7157 18.8598 16.9118 16.3545C19.1772 13.8552 22.1488 12.5719 25.8373 12.5719C30.1064 12.5719 33.3325 14.1955 35.4832 17.4394L37.5587 20.8853L39.6377 17.4394C41.7884 14.1955 45.0145 12.5719 49.2765 12.5719C52.9614 12.5719 55.9329 13.8552 58.2055 16.3545C60.4017 18.8574 61.4997 22.2371 61.4997 26.4937L61.4925 47.3144Z" fill="inherit"></path>
</svg>
</a>
</div>
</li>
</ul>
</nav>
</header>
<script>
window.addEventListener('keydown', function(event) {
if (event.key === "/") {
event.preventDefault();
document.querySelector("input[type='search']").focus()
}
})
</script>
<main class="bg-background dark:bg-dark-background pt-[80px]">
<nav aria-label="breadcrumbs" class="px-4 flex bg-title dark:bg-[#111827] text-white dark:text-dark-title md:hidden">
<ul>
<li class="inline-block">
<a href="http://rocq-prover.org/stdlib" class="flex items-center px-2 py-2 border-transparent border-2 border-b-4"> Standard Library
<span> <svg xmlns="http://www.w3.org/2000/svg" class="w-3 h-3 ml-2" fill="none" viewBox="0 0 24 24" stroke-width="1.5" stroke="currentColor" aria-hidden="true">
<path stroke-linecap="round" stroke-linejoin="round" d="M8.25 4.5l7.5 7.5-7.5 7.5"></path>
</svg>
</span> </a>
</li>
<li class="inline-block">
<select onchange="location = this.value;" class="appearance-none border-2 border-b-4 bg-transparent bg-none font-bold border-none w-auto p-0 m-0 cursor-pointer focus:outline-none focus:ring-0">
<option value="index.html" selected="">
Table of contents
</option>
<option value="genindex.html">
Index
</option>
</select>
<span class="text-primary dark:text-dark-primary cursor-pointer">▾</span>
</li>
</ul>
</nav>
<div class="hidden md:flex">
<nav class="lg:-mt-[10px] lg:pt-[10px] bg-secondary dark:bg-[#111827] rounded-b-lg container-fluid wide flex flex-wrap">
<a href="index.html" class="justify-start px-4 py-2 text-white dark:text-dark-title items-center font-normal border-2 border-b-4 border-transparent rounded border-b-primary dark:border-b-dark-primary">
Table of contents
</a>
<a href="genindex.html" class="justify-start px-4 py-2 text-white dark:text-dark-title items-center font-normal border-2 border-b-4 border-transparent rounded opacity-80 hover:text-primary dark:hover:text-dark-primary">
Index
</a>
</nav>
</div>
<div class="bg-background dark:bg-dark-background">
<div class="flex-1 z-0 z- min-w-0 pb-12">
<div class="bg-background dark:bg-dark-background">
<div class="container-fluid dark:text-dark-content prose pt-10 stdlib text-content">
<!-- ************************
END STDLIB HEADER
************************* -->
|
