-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
0 parents
commit fe78665
Showing
118 changed files
with
10,064 additions
and
0 deletions.
There are no files selected for viewing
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,4 @@ | ||
# Sphinx build info version 1 | ||
# This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done. | ||
config: 0fc2a8f3ba14656c553ca4e2e4ef7ec2 | ||
tags: 645f666f9bcd5a90fca523b33c5a78b7 |
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file added
BIN
+4.6 KB
.doctrees/_autosummary/knuckledragger.notation.lookup_cons_recog.doctree
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Empty file.
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,133 @@ | ||
<!DOCTYPE html> | ||
<html class="writer-html5" lang="en" data-content_root="../"> | ||
<head> | ||
<meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" /> | ||
|
||
<meta name="viewport" content="width=device-width, initial-scale=1.0" /> | ||
<title>knuckledragger — knuckledragger 0.1 documentation</title> | ||
<link rel="stylesheet" type="text/css" href="../_static/pygments.css?v=80d5e7a1" /> | ||
<link rel="stylesheet" type="text/css" href="../_static/css/theme.css?v=19f00094" /> | ||
|
||
|
||
<!--[if lt IE 9]> | ||
<script src="../_static/js/html5shiv.min.js"></script> | ||
<![endif]--> | ||
|
||
<script src="../_static/jquery.js?v=5d32c60e"></script> | ||
<script src="../_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script> | ||
<script src="../_static/documentation_options.js?v=2709fde1"></script> | ||
<script src="../_static/doctools.js?v=9a2dae69"></script> | ||
<script src="../_static/sphinx_highlight.js?v=dc90522c"></script> | ||
<script src="../_static/js/theme.js"></script> | ||
<link rel="index" title="Index" href="../genindex.html" /> | ||
<link rel="search" title="Search" href="../search.html" /> | ||
<link rel="next" title="knuckledragger.kernel" href="knuckledragger.kernel.html" /> | ||
<link rel="prev" title="Welcome to knuckledragger’s documentation!" href="../index.html" /> | ||
</head> | ||
|
||
<body class="wy-body-for-nav"> | ||
<div class="wy-grid-for-nav"> | ||
<nav data-toggle="wy-nav-shift" class="wy-nav-side"> | ||
<div class="wy-side-scroll"> | ||
<div class="wy-side-nav-search" > | ||
|
||
|
||
|
||
<a href="../index.html" class="icon icon-home"> | ||
knuckledragger | ||
</a> | ||
<div role="search"> | ||
<form id="rtd-search-form" class="wy-form" action="../search.html" method="get"> | ||
<input type="text" name="q" placeholder="Search docs" aria-label="Search docs" /> | ||
<input type="hidden" name="check_keywords" value="yes" /> | ||
<input type="hidden" name="area" value="default" /> | ||
</form> | ||
</div> | ||
</div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu"> | ||
<ul class="current"> | ||
<li class="toctree-l1 current"><a class="current reference internal" href="#">knuckledragger</a><ul> | ||
<li class="toctree-l2"><a class="reference internal" href="knuckledragger.kernel.html">knuckledragger.kernel</a></li> | ||
<li class="toctree-l2"><a class="reference internal" href="knuckledragger.notation.html">knuckledragger.notation</a></li> | ||
<li class="toctree-l2"><a class="reference internal" href="knuckledragger.theories.html">knuckledragger.theories</a></li> | ||
<li class="toctree-l2"><a class="reference internal" href="knuckledragger.utils.html">knuckledragger.utils</a></li> | ||
</ul> | ||
</li> | ||
</ul> | ||
|
||
</div> | ||
</div> | ||
</nav> | ||
|
||
<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" > | ||
<i data-toggle="wy-nav-top" class="fa fa-bars"></i> | ||
<a href="../index.html">knuckledragger</a> | ||
</nav> | ||
|
||
<div class="wy-nav-content"> | ||
<div class="rst-content"> | ||
<div role="navigation" aria-label="Page navigation"> | ||
<ul class="wy-breadcrumbs"> | ||
<li><a href="../index.html" class="icon icon-home" aria-label="Home"></a></li> | ||
<li class="breadcrumb-item active">knuckledragger</li> | ||
<li class="wy-breadcrumbs-aside"> | ||
<a href="../_sources/_autosummary/knuckledragger.rst.txt" rel="nofollow"> View page source</a> | ||
</li> | ||
</ul> | ||
<hr/> | ||
</div> | ||
<div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article"> | ||
<div itemprop="articleBody"> | ||
|
||
<section id="module-knuckledragger"> | ||
<span id="knuckledragger"></span><h1>knuckledragger<a class="headerlink" href="#module-knuckledragger" title="Link to this heading"></a></h1> | ||
<p class="rubric">Modules</p> | ||
<table class="autosummary longtable docutils align-default"> | ||
<tbody> | ||
<tr class="row-odd"><td><p><a class="reference internal" href="knuckledragger.kernel.html#module-knuckledragger.kernel" title="knuckledragger.kernel"><code class="xref py py-obj docutils literal notranslate"><span class="pre">kernel</span></code></a></p></td> | ||
<td><p></p></td> | ||
</tr> | ||
<tr class="row-even"><td><p><a class="reference internal" href="knuckledragger.notation.html#module-knuckledragger.notation" title="knuckledragger.notation"><code class="xref py py-obj docutils literal notranslate"><span class="pre">notation</span></code></a></p></td> | ||
<td><p>Importing this module will add some syntactic sugar to Z3.</p></td> | ||
</tr> | ||
<tr class="row-odd"><td><p><a class="reference internal" href="knuckledragger.theories.html#module-knuckledragger.theories" title="knuckledragger.theories"><code class="xref py py-obj docutils literal notranslate"><span class="pre">theories</span></code></a></p></td> | ||
<td><p></p></td> | ||
</tr> | ||
<tr class="row-even"><td><p><a class="reference internal" href="knuckledragger.utils.html#module-knuckledragger.utils" title="knuckledragger.utils"><code class="xref py py-obj docutils literal notranslate"><span class="pre">utils</span></code></a></p></td> | ||
<td><p></p></td> | ||
</tr> | ||
</tbody> | ||
</table> | ||
</section> | ||
|
||
|
||
</div> | ||
</div> | ||
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer"> | ||
<a href="../index.html" class="btn btn-neutral float-left" title="Welcome to knuckledragger’s documentation!" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a> | ||
<a href="knuckledragger.kernel.html" class="btn btn-neutral float-right" title="knuckledragger.kernel" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a> | ||
</div> | ||
|
||
<hr/> | ||
|
||
<div role="contentinfo"> | ||
<p>© Copyright 2024, Philip Zucker.</p> | ||
</div> | ||
|
||
Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a | ||
<a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a> | ||
provided by <a href="https://readthedocs.org">Read the Docs</a>. | ||
|
||
|
||
</footer> | ||
</div> | ||
</div> | ||
</section> | ||
</div> | ||
<script> | ||
jQuery(function () { | ||
SphinxRtdTheme.Navigation.enable(true); | ||
}); | ||
</script> | ||
|
||
</body> | ||
</html> |
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,142 @@ | ||
<!DOCTYPE html> | ||
<html class="writer-html5" lang="en" data-content_root="../"> | ||
<head> | ||
<meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" /> | ||
|
||
<meta name="viewport" content="width=device-width, initial-scale=1.0" /> | ||
<title>knuckledragger.kernel.axiom — knuckledragger 0.1 documentation</title> | ||
<link rel="stylesheet" type="text/css" href="../_static/pygments.css?v=80d5e7a1" /> | ||
<link rel="stylesheet" type="text/css" href="../_static/css/theme.css?v=19f00094" /> | ||
|
||
|
||
<!--[if lt IE 9]> | ||
<script src="../_static/js/html5shiv.min.js"></script> | ||
<![endif]--> | ||
|
||
<script src="../_static/jquery.js?v=5d32c60e"></script> | ||
<script src="../_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script> | ||
<script src="../_static/documentation_options.js?v=2709fde1"></script> | ||
<script src="../_static/doctools.js?v=9a2dae69"></script> | ||
<script src="../_static/sphinx_highlight.js?v=dc90522c"></script> | ||
<script src="../_static/js/theme.js"></script> | ||
<link rel="index" title="Index" href="../genindex.html" /> | ||
<link rel="search" title="Search" href="../search.html" /> | ||
<link rel="next" title="knuckledragger.kernel.define" href="knuckledragger.kernel.define.html" /> | ||
<link rel="prev" title="knuckledragger.kernel" href="knuckledragger.kernel.html" /> | ||
</head> | ||
|
||
<body class="wy-body-for-nav"> | ||
<div class="wy-grid-for-nav"> | ||
<nav data-toggle="wy-nav-shift" class="wy-nav-side"> | ||
<div class="wy-side-scroll"> | ||
<div class="wy-side-nav-search" > | ||
|
||
|
||
|
||
<a href="../index.html" class="icon icon-home"> | ||
knuckledragger | ||
</a> | ||
<div role="search"> | ||
<form id="rtd-search-form" class="wy-form" action="../search.html" method="get"> | ||
<input type="text" name="q" placeholder="Search docs" aria-label="Search docs" /> | ||
<input type="hidden" name="check_keywords" value="yes" /> | ||
<input type="hidden" name="area" value="default" /> | ||
</form> | ||
</div> | ||
</div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu"> | ||
<ul class="current"> | ||
<li class="toctree-l1 current"><a class="reference internal" href="knuckledragger.html">knuckledragger</a><ul class="current"> | ||
<li class="toctree-l2 current"><a class="reference internal" href="knuckledragger.kernel.html">knuckledragger.kernel</a><ul class="current"> | ||
<li class="toctree-l3 current"><a class="current reference internal" href="#">knuckledragger.kernel.axiom</a><ul> | ||
<li class="toctree-l4"><a class="reference internal" href="#knuckledragger.kernel.axiom"><code class="docutils literal notranslate"><span class="pre">axiom()</span></code></a></li> | ||
</ul> | ||
</li> | ||
<li class="toctree-l3"><a class="reference internal" href="knuckledragger.kernel.define.html">knuckledragger.kernel.define</a></li> | ||
<li class="toctree-l3"><a class="reference internal" href="knuckledragger.kernel.is_proof.html">knuckledragger.kernel.is_proof</a></li> | ||
<li class="toctree-l3"><a class="reference internal" href="knuckledragger.kernel.lemma.html">knuckledragger.kernel.lemma</a></li> | ||
</ul> | ||
</li> | ||
<li class="toctree-l2"><a class="reference internal" href="knuckledragger.notation.html">knuckledragger.notation</a></li> | ||
<li class="toctree-l2"><a class="reference internal" href="knuckledragger.theories.html">knuckledragger.theories</a></li> | ||
<li class="toctree-l2"><a class="reference internal" href="knuckledragger.utils.html">knuckledragger.utils</a></li> | ||
</ul> | ||
</li> | ||
</ul> | ||
|
||
</div> | ||
</div> | ||
</nav> | ||
|
||
<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" > | ||
<i data-toggle="wy-nav-top" class="fa fa-bars"></i> | ||
<a href="../index.html">knuckledragger</a> | ||
</nav> | ||
|
||
<div class="wy-nav-content"> | ||
<div class="rst-content"> | ||
<div role="navigation" aria-label="Page navigation"> | ||
<ul class="wy-breadcrumbs"> | ||
<li><a href="../index.html" class="icon icon-home" aria-label="Home"></a></li> | ||
<li class="breadcrumb-item"><a href="knuckledragger.html">knuckledragger</a></li> | ||
<li class="breadcrumb-item"><a href="knuckledragger.kernel.html">knuckledragger.kernel</a></li> | ||
<li class="breadcrumb-item active">knuckledragger.kernel.axiom</li> | ||
<li class="wy-breadcrumbs-aside"> | ||
<a href="../_sources/_autosummary/knuckledragger.kernel.axiom.rst.txt" rel="nofollow"> View page source</a> | ||
</li> | ||
</ul> | ||
<hr/> | ||
</div> | ||
<div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article"> | ||
<div itemprop="articleBody"> | ||
|
||
<section id="knuckledragger-kernel-axiom"> | ||
<h1>knuckledragger.kernel.axiom<a class="headerlink" href="#knuckledragger-kernel-axiom" title="Link to this heading"></a></h1> | ||
<dl class="py function"> | ||
<dt class="sig sig-object py" id="knuckledragger.kernel.axiom"> | ||
<span class="sig-prename descclassname"><span class="pre">knuckledragger.kernel.</span></span><span class="sig-name descname"><span class="pre">axiom</span></span><span class="sig-paren">(</span><em class="sig-param"><span class="n"><span class="pre">thm</span></span><span class="p"><span class="pre">:</span></span><span class="w"> </span><span class="n"><span class="pre">BoolRef</span></span></em>, <em class="sig-param"><span class="n"><span class="pre">by</span></span><span class="o"><span class="pre">=</span></span><span class="default_value"><span class="pre">[]</span></span></em><span class="sig-paren">)</span> <span class="sig-return"><span class="sig-return-icon">→</span> <span class="sig-return-typehint"><span class="pre">None</span></span></span><a class="headerlink" href="#knuckledragger.kernel.axiom" title="Link to this definition"></a></dt> | ||
<dd><p>Assert an axiom.</p> | ||
<p>Axioms are necessary and useful. But you must use great care.</p> | ||
<dl class="field-list simple"> | ||
<dt class="field-odd">Parameters<span class="colon">:</span></dt> | ||
<dd class="field-odd"><ul class="simple"> | ||
<li><p><strong>thm</strong> – The axiom to assert.</p></li> | ||
<li><p><strong>by</strong> – A python object explaining why the axiom should exist. Often a string explaining the axiom.</p></li> | ||
</ul> | ||
</dd> | ||
</dl> | ||
</dd></dl> | ||
|
||
</section> | ||
|
||
|
||
</div> | ||
</div> | ||
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer"> | ||
<a href="knuckledragger.kernel.html" class="btn btn-neutral float-left" title="knuckledragger.kernel" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a> | ||
<a href="knuckledragger.kernel.define.html" class="btn btn-neutral float-right" title="knuckledragger.kernel.define" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a> | ||
</div> | ||
|
||
<hr/> | ||
|
||
<div role="contentinfo"> | ||
<p>© Copyright 2024, Philip Zucker.</p> | ||
</div> | ||
|
||
Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a | ||
<a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a> | ||
provided by <a href="https://readthedocs.org">Read the Docs</a>. | ||
|
||
|
||
</footer> | ||
</div> | ||
</div> | ||
</section> | ||
</div> | ||
<script> | ||
jQuery(function () { | ||
SphinxRtdTheme.Navigation.enable(true); | ||
}); | ||
</script> | ||
|
||
</body> | ||
</html> |
Oops, something went wrong.