Skip to content

Commit

Permalink
deploy: 4829e90
Browse files Browse the repository at this point in the history
  • Loading branch information
@philzook58
philzook58 committed Aug 22, 2024
0 parents commit 491fe8d
Show file tree
Hide file tree
Showing 184 changed files with 14,371 additions and 0 deletions.
4 changes: 4 additions & 0 deletions .buildinfo
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 added .doctrees/_autosummary/knuckledragger.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.kernel.axiom.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.kernel.define.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.kernel.define_fix.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.kernel.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.kernel.is_proof.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.kernel.lemma.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.notation.QExists.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.notation.QForAll.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.notation.Record.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.notation.datatype_call.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.notation.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.notation.lookup_cons_recog.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.smt.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.solvers.binpath.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.solvers.collect_decls.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.solvers.collect_sorts.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.solvers.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.solvers.run.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.solvers.smtlib_datatypes.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.tactics.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.tactics.lemma.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.theories.Complex.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.theories.Int.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.theories.Int.induct_nat.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.theories.Interval.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.theories.Nat.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.theories.Nat.induct.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.theories.Real.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.theories.Seq.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.theories.Seq.induct.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.theories.Vec.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.theories.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.utils.decls.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.utils.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.utils.expr_to_tptp.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.utils.lemma_db.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.utils.lemma_smt.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.utils.lemma_tptp.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.utils.open_binder.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.utils.simp.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.utils.simp2.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.utils.sort_to_tptp.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.utils.sorts.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.utils.subterms.doctree
Binary file not shown.
Binary file added .doctrees/_autosummary/knuckledragger.utils.z3_match.doctree
Binary file not shown.
Binary file added .doctrees/environment.pickle
Binary file not shown.
Binary file added .doctrees/index.doctree
Binary file not shown.
Empty file added .nojekyll
Empty file.
145 changes: 145 additions & 0 deletions _autosummary/knuckledragger.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,145 @@
<!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 &mdash; 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.smt.html">knuckledragger.smt</a></li>
<li class="toctree-l2"><a class="reference internal" href="knuckledragger.solvers.html">knuckledragger.solvers</a></li>
<li class="toctree-l2"><a class="reference internal" href="knuckledragger.tactics.html">knuckledragger.tactics</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 smt.</p></td>
</tr>
<tr class="row-odd"><td><p><a class="reference internal" href="knuckledragger.smt.html#module-knuckledragger.smt" title="knuckledragger.smt"><code class="xref py py-obj docutils literal notranslate"><span class="pre">smt</span></code></a></p></td>
<td><p>This is a shim file to enable the use of cvc5 and vampire as default solvers.</p></td>
</tr>
<tr class="row-even"><td><p><a class="reference internal" href="knuckledragger.solvers.html#module-knuckledragger.solvers" title="knuckledragger.solvers"><code class="xref py py-obj docutils literal notranslate"><span class="pre">solvers</span></code></a></p></td>
<td><p></p></td>
</tr>
<tr class="row-odd"><td><p><a class="reference internal" href="knuckledragger.tactics.html#module-knuckledragger.tactics" title="knuckledragger.tactics"><code class="xref py py-obj docutils literal notranslate"><span class="pre">tactics</span></code></a></p></td>
<td><p></p></td>
</tr>
<tr class="row-even"><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-odd"><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>&#169; 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>
146 changes: 146 additions & 0 deletions _autosummary/knuckledragger.kernel.axiom.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,146 @@
<!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 &mdash; 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.define_fix.html">knuckledragger.kernel.define_fix</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.smt.html">knuckledragger.smt</a></li>
<li class="toctree-l2"><a class="reference internal" href="knuckledragger.solvers.html">knuckledragger.solvers</a></li>
<li class="toctree-l2"><a class="reference internal" href="knuckledragger.tactics.html">knuckledragger.tactics</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">&#x2192;</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>&#169; 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>
Loading

0 comments on commit 491fe8d

Please sign in to comment.