-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Documentation of branch “v9.0” at 147fa795
- Loading branch information
Showing
700 changed files
with
325,784 additions
and
1,870 deletions.
There are no files selected for viewing
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,128 @@ | ||
| <!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" lang="en" xml:lang="en"> | ||
|
|
||
| <head> | ||
| <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> | ||
| <link rel="shortcut icon" href="/favicon.ico" type="image/x-icon" /> | ||
| <link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/node/node.css" /> | ||
| <link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/system/defaults.css" /> | ||
| <link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/system/system.css" /> | ||
| <link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/user/user.css" /> | ||
| <link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/sites/all/themes/coq/style.css" /> | ||
| <link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/sites/all/themes/coq/coqdoc.css" /> | ||
|
|
||
| <title>Standard Library | The Coq Proof Assistant</title> | ||
|
|
||
| </head> | ||
|
|
||
| <body> | ||
|
|
||
| <div id="container"> | ||
| <div id="headertop"> | ||
| <div id="nav"> | ||
| <ul class="links-menu"> | ||
| <li><a href="//coq.inria.fr/" class="active">Home</a></li> | ||
| <li><a href="//coq.inria.fr/about-coq" title="More about coq">About Coq</a></li> | ||
| <li><a href="//coq.inria.fr/download">Get Coq</a></li> | ||
| <li><a href="//coq.inria.fr/documentation">Documentation</a></li> | ||
| <li><a href="//coq.inria.fr/community">Community</a></li> | ||
| </ul> | ||
| </div> | ||
| </div> | ||
|
|
||
| <div id="header"> | ||
| <div id="logoWrapper"> | ||
| <div id="logo"><a href="//coq.inria.fr/" title="Home"><img src="//coq.inria.fr/files/barron_logo.png" alt="Home" /></a> | ||
| </div> | ||
| <div id="siteName"><a href="//coq.inria.fr/" title="Home">The Coq Proof Assistant</a> | ||
| </div> | ||
| </div> | ||
| </div> | ||
|
|
||
| <div id="content"> | ||
|
|
||
| <h1 class="libtitle">Library Corelib.Array.PrimArray</h1> | ||
|
|
||
| <div class="code"> | ||
| <span class="id" title="keyword">From</span> <span class="id" title="var">Corelib</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Corelib.Numbers.Cyclic.Int63.PrimInt63.html#"><span class="id" title="library">PrimInt63</span></a>.<br/> | ||
|
|
||
| <br/> | ||
|
|
||
| <br/> | ||
| <span class="id" title="keyword">Primitive</span> <a id="array" class="idref" href="#array"><span class="id" title="axiom">array</span></a> := #<span class="id" title="var">array_type</span>.<br/> | ||
|
|
||
| <br/> | ||
| <span class="id" title="keyword">Primitive</span> <a id="make" class="idref" href="#make"><span class="id" title="axiom">make</span></a> : <span class="id" title="keyword">forall</span> <a id="A:1" class="idref" href="#A:1"><span class="id" title="binder">A</span></a>, <span class="id" title="var">int</span> <a class="idref" href="Corelib.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Corelib.Array.PrimArray.html#A:1"><span class="id" title="variable">A</span></a> <a class="idref" href="Corelib.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <span class="id" title="var">array</span> <a class="idref" href="Corelib.Array.PrimArray.html#A:1"><span class="id" title="variable">A</span></a> := #<span class="id" title="var">array_make</span>.<br/> | ||
| <span class="id" title="keyword">Arguments</span> <span class="id" title="var">make</span> {<span class="id" title="var">_</span>} <span class="id" title="var">_</span> <span class="id" title="var">_</span>.<br/> | ||
|
|
||
| <br/> | ||
| <span class="id" title="keyword">Primitive</span> <a id="get" class="idref" href="#get"><span class="id" title="axiom">get</span></a> : <span class="id" title="keyword">forall</span> <a id="A:2" class="idref" href="#A:2"><span class="id" title="binder">A</span></a>, <span class="id" title="var">array</span> <a class="idref" href="Corelib.Array.PrimArray.html#A:2"><span class="id" title="variable">A</span></a> <a class="idref" href="Corelib.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <span class="id" title="var">int</span> <a class="idref" href="Corelib.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Corelib.Array.PrimArray.html#A:2"><span class="id" title="variable">A</span></a> := #<span class="id" title="var">array_get</span>.<br/> | ||
| <span class="id" title="keyword">Arguments</span> <span class="id" title="var">get</span> {<span class="id" title="var">_</span>} <span class="id" title="var">_</span> <span class="id" title="var">_</span>.<br/> | ||
|
|
||
| <br/> | ||
| <span class="id" title="keyword">Primitive</span> <a id="default" class="idref" href="#default"><span class="id" title="axiom">default</span></a> : <span class="id" title="keyword">forall</span> <a id="A:3" class="idref" href="#A:3"><span class="id" title="binder">A</span></a>, <span class="id" title="var">array</span> <a class="idref" href="Corelib.Array.PrimArray.html#A:3"><span class="id" title="variable">A</span></a> <a class="idref" href="Corelib.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Corelib.Array.PrimArray.html#A:3"><span class="id" title="variable">A</span></a>:= #<span class="id" title="var">array_default</span>.<br/> | ||
| <span class="id" title="keyword">Arguments</span> <span class="id" title="var">default</span> {<span class="id" title="var">_</span>} <span class="id" title="var">_</span>.<br/> | ||
|
|
||
| <br/> | ||
| <span class="id" title="keyword">Primitive</span> <a id="set" class="idref" href="#set"><span class="id" title="axiom">set</span></a> : <span class="id" title="keyword">forall</span> <a id="A:4" class="idref" href="#A:4"><span class="id" title="binder">A</span></a>, <span class="id" title="var">array</span> <a class="idref" href="Corelib.Array.PrimArray.html#A:4"><span class="id" title="variable">A</span></a> <a class="idref" href="Corelib.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <span class="id" title="var">int</span> <a class="idref" href="Corelib.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Corelib.Array.PrimArray.html#A:4"><span class="id" title="variable">A</span></a> <a class="idref" href="Corelib.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <span class="id" title="var">array</span> <a class="idref" href="Corelib.Array.PrimArray.html#A:4"><span class="id" title="variable">A</span></a> := #<span class="id" title="var">array_set</span>.<br/> | ||
| <span class="id" title="keyword">Arguments</span> <span class="id" title="tactic">set</span> {<span class="id" title="var">_</span>} <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span>.<br/> | ||
|
|
||
| <br/> | ||
| <span class="id" title="keyword">Primitive</span> <a id="length" class="idref" href="#length"><span class="id" title="axiom">length</span></a> : <span class="id" title="keyword">forall</span> <a id="A:5" class="idref" href="#A:5"><span class="id" title="binder">A</span></a>, <span class="id" title="var">array</span> <a class="idref" href="Corelib.Array.PrimArray.html#A:5"><span class="id" title="variable">A</span></a> <a class="idref" href="Corelib.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <span class="id" title="var">int</span> := #<span class="id" title="var">array_length</span>.<br/> | ||
| <span class="id" title="keyword">Arguments</span> <span class="id" title="var">length</span> {<span class="id" title="var">_</span>} <span class="id" title="var">_</span>.<br/> | ||
|
|
||
| <br/> | ||
| <span class="id" title="keyword">Primitive</span> <a id="copy" class="idref" href="#copy"><span class="id" title="axiom">copy</span></a> : <span class="id" title="keyword">forall</span> <a id="A:6" class="idref" href="#A:6"><span class="id" title="binder">A</span></a>, <span class="id" title="var">array</span> <a class="idref" href="Corelib.Array.PrimArray.html#A:6"><span class="id" title="variable">A</span></a> <a class="idref" href="Corelib.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <span class="id" title="var">array</span> <a class="idref" href="Corelib.Array.PrimArray.html#A:6"><span class="id" title="variable">A</span></a> := #<span class="id" title="var">array_copy</span>.<br/> | ||
| <span class="id" title="keyword">Arguments</span> <span class="id" title="var">copy</span> {<span class="id" title="var">_</span>} <span class="id" title="var">_</span>.<br/> | ||
|
|
||
| <br/> | ||
| <span class="id" title="keyword">Module</span> <span class="id" title="keyword">Export</span> <a id="PArrayNotations" class="idref" href="#PArrayNotations"><span class="id" title="module">PArrayNotations</span></a>.<br/> | ||
|
|
||
| <br/> | ||
| <span class="id" title="keyword">Declare Scope</span> <span class="id" title="var">array_scope</span>.<br/> | ||
| <span class="id" title="keyword">Delimit</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">array_scope</span> <span class="id" title="keyword">with</span> <span class="id" title="var">array</span>.<br/> | ||
| <span class="id" title="keyword">Notation</span> <a id="8e02ba31407e3638944c90e7c0afd5c3" class="idref" href="#8e02ba31407e3638944c90e7c0afd5c3"><span class="id" title="notation">"</span></a>t .[ i ]" := (<span class="id" title="var">get</span> <span class="id" title="var">t</span> <span class="id" title="var">i</span>)<br/> | ||
| (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>, <span class="id" title="var">format</span> "t .[ i ]").<br/> | ||
| <span class="id" title="keyword">Notation</span> <a id="bff3894582fa3645cf662c9c1a220f5d" class="idref" href="#bff3894582fa3645cf662c9c1a220f5d"><span class="id" title="notation">"</span></a>t .[ i <- a ]" := (<span class="id" title="tactic">set</span> <span class="id" title="var">t</span> <span class="id" title="var">i</span> <span class="id" title="var">a</span>)<br/> | ||
| (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>, <span class="id" title="var">format</span> "t .[ i <- a ]").<br/> | ||
|
|
||
| <br/> | ||
| <span class="id" title="keyword">End</span> <a class="idref" href="Corelib.Array.PrimArray.html#PArrayNotations"><span class="id" title="module">PArrayNotations</span></a>.<br/> | ||
|
|
||
| <br/> | ||
| <span class="id" title="keyword">Primitive</span> <a id="max_length" class="idref" href="#max_length"><span class="id" title="axiom">max_length</span></a> := #<span class="id" title="var">array_max_length</span>.<br/> | ||
| </div> | ||
| <div id="sidebarWrapper"> | ||
| <div id="sidebar"> | ||
| <div class="block"> | ||
| <h2 class="title">Navigation</h2> | ||
| <div class="content"> | ||
| <ul class="menu"> | ||
| <li class="leaf">Standard Library | ||
| <ul class="menu"> | ||
| <li><a href="index.html">Table of contents</a></li> | ||
| <li><a href="genindex.html">Index</a></li> | ||
| </ul> | ||
| </li> | ||
| </ul> | ||
| </div> | ||
| </div> | ||
| </div> | ||
| </div> | ||
|
|
||
| </div> | ||
|
|
||
| <div id="footer"> | ||
| <div id="nav-footer"> | ||
| <ul class="links-menu-footer"> | ||
| <li><a href="mailto:coq-www_@_inria.fr">webmaster</a></li> | ||
| <li><a href="http://validator.w3.org/">xhtml valid</a></li> | ||
| <li><a href="http://jigsaw.w3.org/css-validator/">CSS valid</a></li> | ||
| </ul> | ||
| </div> | ||
| </div> | ||
|
|
||
| </div> | ||
|
|
||
| </body> | ||
| </html> |
Oops, something went wrong.