Skip to content

Commit

Permalink
Deploying to gh-pages from @ cb61d68 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
Ailrun committed Oct 1, 2024
1 parent 97defb7 commit 8de745c
Show file tree
Hide file tree
Showing 32 changed files with 11,681 additions and 0 deletions.
48 changes: 48 additions & 0 deletions ext/prop-eq/Mcltt.Core.Base.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
<!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="./dep.html"> Table of Contents </a>
</span>
</div>
<div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
<div id="main">
<h1 class="libtitle">Mcltt.Core.Base</h1>

<div class="code">
#[<span class="id" title="var">global</span>] <span class="id" title="var">Declare</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">mcltt_scope</span>.<br/>
#[<span class="id" title="var">global</span>] <span class="id" title="keyword">Delimit</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">mcltt_scope</span> <span class="id" title="keyword">with</span> <span class="id" title="var">mcltt</span>.<br/>
#[<span class="id" title="var">global</span>] <span class="id" title="keyword">Bind</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">mcltt_scope</span> <span class="id" title="keyword">with</span> <span class="id" title="var">Sortclass</span>.<br/>

<br/>
#[<span class="id" title="var">global</span>] <span class="id" title="var">Declare</span> <span class="id" title="var">Custom</span> <span class="id" title="var">Entry</span> <span class="id" title="var">judg</span>.<br/>

<br/>
<span class="id" title="keyword">Notation</span> <a id="2e12ae37c5a5c7396a13d7170e0de451" class="idref" href="#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">&quot;</span></a>{{ x }}" := <span class="id" title="var">x</span> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">x</span> <span class="id" title="var">custom</span> <span class="id" title="var">judg</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99, <span class="id" title="var">format</span> "'{{' x '}}'").<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>
228 changes: 228 additions & 0 deletions ext/prop-eq/Mcltt.Core.Syntactic.CoreInversions.html

Large diffs are not rendered by default.

105 changes: 105 additions & 0 deletions ext/prop-eq/Mcltt.Core.Syntactic.CoreTypeInversions.html

Large diffs are not rendered by default.

607 changes: 607 additions & 0 deletions ext/prop-eq/Mcltt.Core.Syntactic.Corollaries.html

Large diffs are not rendered by default.

155 changes: 155 additions & 0 deletions ext/prop-eq/Mcltt.Core.Syntactic.CtxEq.html

Large diffs are not rendered by default.

249 changes: 249 additions & 0 deletions ext/prop-eq/Mcltt.Core.Syntactic.CtxSub.html

Large diffs are not rendered by default.

1,506 changes: 1,506 additions & 0 deletions ext/prop-eq/Mcltt.Core.Syntactic.Presup.html

Large diffs are not rendered by default.

321 changes: 321 additions & 0 deletions ext/prop-eq/Mcltt.Core.Syntactic.Syntax.html

Large diffs are not rendered by default.

753 changes: 753 additions & 0 deletions ext/prop-eq/Mcltt.Core.Syntactic.System.Definitions.html

Large diffs are not rendered by default.

1,569 changes: 1,569 additions & 0 deletions ext/prop-eq/Mcltt.Core.Syntactic.System.Lemmas.html

Large diffs are not rendered by default.

73 changes: 73 additions & 0 deletions ext/prop-eq/Mcltt.Core.Syntactic.System.Tactics.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,73 @@
<!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="./dep.html"> Table of Contents </a>
</span>
</div>
<div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
<div id="main">
<h1 class="libtitle">Mcltt.Core.Syntactic.System.Tactics</h1>

<div class="code">
<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.LibTactics.html#"><span class="id" title="library">LibTactics</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Base.html#"><span class="id" title="library">Base</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core.Syntactic.System</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#"><span class="id" title="library">Definitions</span></a> <a class="idref" href="Mcltt.Core.Syntactic.System.Lemmas.html#"><span class="id" title="library">Lemmas</span></a>.<br/>
<span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#Syntax_Notations"><span class="id" title="module">Syntax_Notations</span></a>.<br/>

<br/>
#[<span class="id" title="var">global</span>]<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">pi_univ_level_tac</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;| |- <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a><span class="id" title="var">_</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#fc206822ef077f61c7a4810f3d1aab63"><span class="id" title="notation"></span></a><a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#fc206822ef077f61c7a4810f3d1aab63"><span class="id" title="notation">s</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a><span class="id" title="var">_</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#fc206822ef077f61c7a4810f3d1aab63"><span class="id" title="notation">:</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a><span class="id" title="var">_</span> <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> =&gt; <span class="id" title="var">mauto</span> 4<br/>
&nbsp;&nbsp;| <span class="id" title="var">H</span> : <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?<span class="id" title="var">Δ</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#946b41ceb8284bcfce58d31084906f52"><span class="id" title="notation"></span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?<span class="id" title="var">A</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#946b41ceb8284bcfce58d31084906f52"><span class="id" title="notation">:</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#51477920c762bb573d0c48e88bde2399"><span class="id" title="notation">Type@</span></a>?<span class="id" title="var">j</span> <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> |- <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?<span class="id" title="var">Δ</span> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#d1064cbf3bcb4d3b63e8559a3ab3b23c"><span class="id" title="notation">,</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?<span class="id" title="var">A</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#946b41ceb8284bcfce58d31084906f52"><span class="id" title="notation"></span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?<span class="id" title="var">B</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#946b41ceb8284bcfce58d31084906f52"><span class="id" title="notation">:</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#51477920c762bb573d0c48e88bde2399"><span class="id" title="notation">Type@</span></a>?<span class="id" title="var">i</span> <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Lemmas.html#lift_exp_max_right"><span class="id" title="lemma">lift_exp_max_right</span></a>; <span class="id" title="var">mauto</span> 4<br/>
&nbsp;&nbsp;| |- <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?<span class="id" title="var">Δ</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#946b41ceb8284bcfce58d31084906f52"><span class="id" title="notation"></span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?<span class="id" title="var">A</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#946b41ceb8284bcfce58d31084906f52"><span class="id" title="notation">:</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#51477920c762bb573d0c48e88bde2399"><span class="id" title="notation">Type@</span></a>?<span class="id" title="var">j</span> <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Lemmas.html#lift_exp_max_left"><span class="id" title="lemma">lift_exp_max_left</span></a>; <span class="id" title="var">mauto</span> 4<br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>

<br/>
#[<span class="id" title="var">export</span>]<br/>
<span class="id" title="keyword">Hint</span> <span class="id" title="keyword">Rewrite</span> -&gt; <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#wf_exp_eq_pi_sub"><span class="id" title="constructor">wf_exp_eq_pi_sub</span></a> <span class="id" title="keyword">using</span> <span class="id" title="var">pi_univ_level_tac</span> : <span class="id" title="var">mcltt</span>.<br/>

<br/>
#[<span class="id" title="var">local</span>]<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">invert_wf_ctx1</span> <span class="id" title="var">H</span> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <span class="id" title="keyword">type</span> <span class="id" title="keyword">of</span> <span class="id" title="var">H</span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#5bb0e34309fa0f2c1cf8cfc5347d711a"><span class="id" title="notation"></span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a><span class="id" title="var">_</span> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#d1064cbf3bcb4d3b63e8559a3ab3b23c"><span class="id" title="notation">,</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a><span class="id" title="var">_</span> <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="var">H'</span> := <span class="id" title="tactic">fresh</span> "H" <span class="id" title="tactic">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">pose</span> <span class="id" title="var">proof</span> <span class="id" title="var">H</span> <span class="id" title="keyword">as</span> <span class="id" title="var">H'</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">progressive_invert</span> <span class="id" title="var">H'</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>

<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">invert_wf_ctx</span> :=<br/>
&nbsp;&nbsp;(<span class="id" title="var">on_all_hyp</span>: <span class="id" title="keyword">fun</span> <span class="id" title="var">H</span> =&gt; <span class="id" title="var">invert_wf_ctx1</span> <span class="id" title="var">H</span>);<br/>
&nbsp;&nbsp;<span class="id" title="var">clear_dups</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>
40 changes: 40 additions & 0 deletions ext/prop-eq/Mcltt.Core.Syntactic.System.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
<!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="./dep.html"> Table of Contents </a>
</span>
</div>
<div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
<div id="main">
<h1 class="libtitle">Mcltt.Core.Syntactic.System</h1>

<div class="code">
<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core.Syntactic.System</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#"><span class="id" title="library">Definitions</span></a> <a class="idref" href="Mcltt.Core.Syntactic.System.Lemmas.html#"><span class="id" title="library">Lemmas</span></a> <a class="idref" href="Mcltt.Core.Syntactic.System.Tactics.html#"><span class="id" title="library">Tactics</span></a>.<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>
Loading

0 comments on commit 8de745c

Please sign in to comment.