Add v0.12.2 and v0.13.0

coq-community · Dec 9, 2024 · c318d41 · c318d41
1 parent 2902eba
commit c318d41
Show file tree

Hide file tree

Showing 243 changed files with 44,417 additions and 0 deletions.
diff --git a/index.html b/index.html
@@ -212,6 +212,8 @@ <h2 id="authors-and-contributors">Authors and contributors</h2>
 </ul>
 <h2 id="documentation-1">Documentation</h2>
 <ul>
+<li><a href="v0.13.0/toc.html">0.13.0</a></li>
+<li><a href="v0.12.2/toc.html">0.12.2</a></li>
 <li><a href="v0.12.1/toc.html">0.12.1</a></li>
 <li><a href="v0.12.0/toc.html">0.12.0</a></li>
 <li><a href="v0.11.8/toc.html">0.11.8</a></li>

diff --git a/v0.12.2/ExtLib.Core.Any.html b/v0.12.2/ExtLib.Core.Any.html
@@ -0,0 +1,63 @@
+<!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="resources/coqdoc.css" rel="stylesheet" type="text/css" />
+<link href="resources/coqdocjs.css" rel="stylesheet" type="text/css"/>
+<script type="text/javascript" src="resources/config.js"></script>
+<script type="text/javascript" src="resources/coqdocjs.js"></script>
+</head>
+
+<body onload="document.getElementById('content').focus()">
+  <div id="header">
+    <span class="left">
+      <span class="modulename"> <script> document.write(document.title) </script> </span>
+    </span>
+
+    <span class="button" id="toggle-proofs"></span>
+
+    <span class="right">
+      <a href="../">Project Page</a>
+      <a href="./indexpage.html"> Index </a>
+      <a href="./toc.html"> Table of Contents </a>
+    </span>
+</div>
+    <div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
+    <div id="main">
+<h1 class="libtitle">ExtLib.Core.Any</h1>
+
+<div class="code">
+<span class="id" title="keyword">Set Implicit Arguments</span>.<br/>
+<span class="id" title="keyword">Set</span> <span class="id" title="keyword">Strict</span> <span class="id" title="keyword">Implicit</span>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+This class should be used when no requirements are needed 
+</div>
+<div class="code">
+<span class="id" title="keyword">Polymorphic Class</span> <a id="Any" class="idref" href="#Any"><span class="id" title="record">Any</span></a> (<a id="T:1" class="idref" href="#T:1"><span class="id" title="binder">T</span></a> : <span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Prop</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Global Polymorphic Instance</span> <a id="Any_a" class="idref" href="#Any_a"><span class="id" title="instance">Any_a</span></a> (<a id="T:3" class="idref" href="#T:3"><span class="id" title="binder">T</span></a> : <span class="id" title="keyword">Type</span>) : <a class="idref" href="ExtLib.Core.Any.html#Any"><span class="id" title="class">Any</span></a> <a class="idref" href="ExtLib.Core.Any.html#T:3"><span class="id" title="variable">T</span></a> := {}.<br/>
+
+<br/>
+<span class="id" title="keyword">Polymorphic Definition</span> <a id="RESOLVE" class="idref" href="#RESOLVE"><span class="id" title="definition">RESOLVE</span></a> (<a id="T:4" class="idref" href="#T:4"><span class="id" title="binder">T</span></a> : <span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> := <a class="idref" href="ExtLib.Core.Any.html#T:4"><span class="id" title="variable">T</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Existing Class</span> <a class="idref" href="ExtLib.Core.Any.html#RESOLVE"><span class="id" title="definition">RESOLVE</span></a>.<br/>
+
+<br/>
+#[<span class="id" title="var">global</span>]<br/>
+<span class="id" title="keyword">Hint</span> <span class="id" title="keyword">Extern</span> 0 (<a class="idref" href="ExtLib.Core.Any.html#RESOLVE"><span class="id" title="class">RESOLVE</span></a> <span class="id" title="var">_</span>) =&gt; <span class="id" title="tactic">unfold</span> <a class="idref" href="ExtLib.Core.Any.html#RESOLVE"><span class="id" title="class">RESOLVE</span></a> : <span class="id" title="var">typeclass_instances</span>.<br/>
+</div>
+</div>
+<div id="footer">
+  Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/coq-community/coqdocjs">CoqdocJS</a>
+</div>
+</div>
+</body>
+
+</html>
diff --git a/v0.12.2/ExtLib.Core.CmpDec.html b/v0.12.2/ExtLib.Core.CmpDec.html
diff --git a/v0.12.2/ExtLib.Core.Decision.html b/v0.12.2/ExtLib.Core.Decision.html
@@ -0,0 +1,65 @@
+<!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="resources/coqdoc.css" rel="stylesheet" type="text/css" />
+<link href="resources/coqdocjs.css" rel="stylesheet" type="text/css"/>
+<script type="text/javascript" src="resources/config.js"></script>
+<script type="text/javascript" src="resources/coqdocjs.js"></script>
+</head>
+
+<body onload="document.getElementById('content').focus()">
+  <div id="header">
+    <span class="left">
+      <span class="modulename"> <script> document.write(document.title) </script> </span>
+    </span>
+
+    <span class="button" id="toggle-proofs"></span>
+
+    <span class="right">
+      <a href="../">Project Page</a>
+      <a href="./indexpage.html"> Index </a>
+      <a href="./toc.html"> Table of Contents </a>
+    </span>
+</div>
+    <div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
+    <div id="main">
+<h1 class="libtitle">ExtLib.Core.Decision</h1>
+
+<div class="code">
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Classes.DecidableClass.html#"><span class="id" title="library">Coq.Classes.DecidableClass</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a id="decideP" class="idref" href="#decideP"><span class="id" title="definition">decideP</span></a> (<a id="P:1" class="idref" href="#P:1"><span class="id" title="binder">P</span></a> : <span class="id" title="keyword">Prop</span>) {<a id="D:2" class="idref" href="#D:2"><span class="id" title="binder">D</span></a> : <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Classes.DecidableClass.html#Decidable"><span class="id" title="class">Decidable</span></a> <a class="idref" href="ExtLib.Core.Decision.html#P:1"><span class="id" title="variable">P</span></a>} : <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">{</span></a><a class="idref" href="ExtLib.Core.Decision.html#P:1"><span class="id" title="variable">P</span></a><a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">+</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#63a68285c81db8f9bc456233bb9ed181"><span class="id" title="notation">~</span></a><a class="idref" href="ExtLib.Core.Decision.html#P:1"><span class="id" title="variable">P</span></a><a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">}</span></a> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">match</span> @<a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Classes.DecidableClass.html#Decidable_witness"><span class="id" title="method">Decidable_witness</span></a> <a class="idref" href="ExtLib.Core.Decision.html#P:1"><span class="id" title="variable">P</span></a> <a class="idref" href="ExtLib.Core.Decision.html#D:2"><span class="id" title="variable">D</span></a> <span class="id" title="keyword">as</span> <span class="id" title="var">X</span> <span class="id" title="keyword">return</span> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="ExtLib.Core.Decision.html#X:3"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Core.Decision.html#P:1"><span class="id" title="variable">P</span></a><a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="ExtLib.Core.Decision.html#X:3"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#63a68285c81db8f9bc456233bb9ed181"><span class="id" title="notation">~</span></a><a class="idref" href="ExtLib.Core.Decision.html#P:1"><span class="id" title="variable">P</span></a><a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">{</span></a><a class="idref" href="ExtLib.Core.Decision.html#P:1"><span class="id" title="variable">P</span></a><a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">+</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#63a68285c81db8f9bc456233bb9ed181"><span class="id" title="notation">~</span></a><a class="idref" href="ExtLib.Core.Decision.html#P:1"><span class="id" title="variable">P</span></a><a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">}</span></a> <span class="id" title="keyword">with</span><br/>
+&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> =&gt; <span class="id" title="keyword">fun</span> <a id="pf:4" class="idref" href="#pf:4"><span class="id" title="binder">pf</span></a> <span class="id" title="var">_</span> =&gt; <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Specif.html#left"><span class="id" title="constructor">left</span></a> (<a class="idref" href="ExtLib.Core.Decision.html#pf:4"><span class="id" title="variable">pf</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#eq_refl"><span class="id" title="constructor">eq_refl</span></a>)<br/>
+&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> =&gt; <span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> <a id="pf:5" class="idref" href="#pf:5"><span class="id" title="binder">pf</span></a> =&gt; <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Specif.html#right"><span class="id" title="constructor">right</span></a> (<a class="idref" href="ExtLib.Core.Decision.html#pf:5"><span class="id" title="variable">pf</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#eq_refl"><span class="id" title="constructor">eq_refl</span></a>)<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">end</span> (@<a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Classes.DecidableClass.html#Decidable_sound"><span class="id" title="lemma">Decidable_sound</span></a> <span class="id" title="var">_</span> <a class="idref" href="ExtLib.Core.Decision.html#D:2"><span class="id" title="variable">D</span></a>) (@<a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Classes.DecidableClass.html#Decidable_complete_alt"><span class="id" title="lemma">Decidable_complete_alt</span></a> <span class="id" title="var">_</span> <a class="idref" href="ExtLib.Core.Decision.html#D:2"><span class="id" title="variable">D</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Ltac</span> <span class="id" title="var">cases_ifd</span> <span class="id" title="var">Hn</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">match</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;|- <span class="id" title="keyword">context</span>[<span class="id" title="keyword">if</span> ?<span class="id" title="var">d</span> <span class="id" title="keyword">then</span> ?<span class="id" title="var">tt</span> <span class="id" title="keyword">else</span> ?<span class="id" title="var">ff</span>] =&gt;<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="var">Hnt</span> := <span class="id" title="tactic">fresh</span> <span class="id" title="var">Hn</span> "t" <span class="id" title="tactic">in</span><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="var">Hnf</span> := <span class="id" title="tactic">fresh</span> <span class="id" title="var">Hn</span> "f" <span class="id" title="tactic">in</span><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">d</span> <span class="id" title="keyword">as</span> [<span class="id" title="var">Hnt</span> | <span class="id" title="var">Hnf</span>] <span class="id" title="keyword">end</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a id="decide_decideP" class="idref" href="#decide_decideP"><span class="id" title="lemma">decide_decideP</span></a>  {<a id="P:6" class="idref" href="#P:6"><span class="id" title="binder">P</span></a>:<span class="id" title="keyword">Prop</span> }`{<a id="H:7" class="idref" href="#H:7"><span class="id" title="binder">Decidable</span></a> <a id="H:7" class="idref" href="#H:7"><span class="id" title="binder">P</span></a>} {<a id="R:8" class="idref" href="#R:8"><span class="id" title="binder">R</span></a>:<span class="id" title="keyword">Type</span>} (<a id="a:9" class="idref" href="#a:9"><span class="id" title="binder">a</span></a> <a id="b:10" class="idref" href="#b:10"><span class="id" title="binder">b</span></a> : <a class="idref" href="ExtLib.Core.Decision.html#R:8"><span class="id" title="variable">R</span></a>) :<br/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><span class="id" title="keyword">if</span> (<a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Classes.DecidableClass.html#decide"><span class="id" title="definition">decide</span></a> <a class="idref" href="ExtLib.Core.Decision.html#P:6"><span class="id" title="variable">P</span></a>) <span class="id" title="keyword">then</span>  <a class="idref" href="ExtLib.Core.Decision.html#a:9"><span class="id" title="variable">a</span></a> <span class="id" title="keyword">else</span> <a class="idref" href="ExtLib.Core.Decision.html#b:10"><span class="id" title="variable">b</span></a><a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><span class="id" title="keyword">if</span> (<a class="idref" href="ExtLib.Core.Decision.html#decideP"><span class="id" title="definition">decideP</span></a> <a class="idref" href="ExtLib.Core.Decision.html#P:6"><span class="id" title="variable">P</span></a>) <span class="id" title="keyword">then</span>  <a class="idref" href="ExtLib.Core.Decision.html#a:9"><span class="id" title="variable">a</span></a> <span class="id" title="keyword">else</span> <a class="idref" href="ExtLib.Core.Decision.html#b:10"><span class="id" title="variable">b</span></a><a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<br/>
+<span class="id" title="keyword">Proof</span>.<br/>
+&nbsp;&nbsp;<span class="id" title="tactic">symmetry</span>. <span class="id" title="tactic">unfold</span> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Classes.DecidableClass.html#decide"><span class="id" title="definition">decide</span></a>.<br/>
+&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> (<a class="idref" href="ExtLib.Core.Decision.html#decideP"><span class="id" title="definition">decideP</span></a> <span class="id" title="var">P</span>).<br/>
+- <span class="id" title="tactic">rewrite</span> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Classes.DecidableClass.html#Decidable_complete"><span class="id" title="lemma">Decidable_complete</span></a>; <span class="id" title="tactic">auto</span>.<br/>
+- <span class="id" title="tactic">rewrite</span> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Classes.DecidableClass.html#Decidable_sound_alt"><span class="id" title="lemma">Decidable_sound_alt</span></a>; <span class="id" title="tactic">auto</span>.<br/>
+<span class="id" title="keyword">Qed</span>.<br/>
+</div>
+</div>
+<div id="footer">
+  Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/coq-community/coqdocjs">CoqdocJS</a>
+</div>
+</div>
+</body>
+
+</html>