deploy: 2bc5f1e

philzook58 · Jan 24, 2025 · dd651bd · dd651bd
commit dd651bd
Show file tree

Hide file tree

Showing 603 changed files with 54,556 additions and 0 deletions.
diff --git a/.buildinfo b/.buildinfo
@@ -0,0 +1,4 @@
+# Sphinx build info version 1
+# This file records the configuration used when building these files. When it is not found, a full rebuild will be done.
+config: 5199709052bf04b18b2737cc91ba3fa7
+tags: 645f666f9bcd5a90fca523b33c5a78b7
diff --git a/.doctrees/_autosummary/kdrag.all.doctree b/.doctrees/_autosummary/kdrag.all.doctree
diff --git a/.doctrees/_autosummary/kdrag.config.doctree b/.doctrees/_autosummary/kdrag.config.doctree
diff --git a/.doctrees/_autosummary/kdrag.datatype.Enum.doctree b/.doctrees/_autosummary/kdrag.datatype.Enum.doctree
diff --git a/.doctrees/_autosummary/kdrag.datatype.Inductive.doctree b/.doctrees/_autosummary/kdrag.datatype.Inductive.doctree
diff --git a/.doctrees/_autosummary/kdrag.datatype.InductiveRel.doctree b/.doctrees/_autosummary/kdrag.datatype.InductiveRel.doctree
diff --git a/.doctrees/_autosummary/kdrag.datatype.NewType.doctree b/.doctrees/_autosummary/kdrag.datatype.NewType.doctree
diff --git a/.doctrees/_autosummary/kdrag.datatype.Record.doctree b/.doctrees/_autosummary/kdrag.datatype.Record.doctree
diff --git a/.doctrees/_autosummary/kdrag.datatype.accessor_num.doctree b/.doctrees/_autosummary/kdrag.datatype.accessor_num.doctree
diff --git a/.doctrees/_autosummary/kdrag.datatype.constructor_num.doctree b/.doctrees/_autosummary/kdrag.datatype.constructor_num.doctree
diff --git a/.doctrees/_autosummary/kdrag.datatype.datatype_call.doctree b/.doctrees/_autosummary/kdrag.datatype.datatype_call.doctree
diff --git a/.doctrees/_autosummary/kdrag.datatype.datatype_iter.doctree b/.doctrees/_autosummary/kdrag.datatype.datatype_iter.doctree
diff --git a/.doctrees/_autosummary/kdrag.datatype.datatype_len.doctree b/.doctrees/_autosummary/kdrag.datatype.datatype_len.doctree
diff --git a/.doctrees/_autosummary/kdrag.datatype.datatype_match_.doctree b/.doctrees/_autosummary/kdrag.datatype.datatype_match_.doctree
diff --git a/.doctrees/_autosummary/kdrag.datatype.datatype_replace.doctree b/.doctrees/_autosummary/kdrag.datatype.datatype_replace.doctree
diff --git a/.doctrees/_autosummary/kdrag.datatype.doctree b/.doctrees/_autosummary/kdrag.datatype.doctree
diff --git a/.doctrees/_autosummary/kdrag.datatype.induct_inductive.doctree b/.doctrees/_autosummary/kdrag.datatype.induct_inductive.doctree
diff --git a/.doctrees/_autosummary/kdrag.datatype.multipattern_match.doctree b/.doctrees/_autosummary/kdrag.datatype.multipattern_match.doctree
diff --git a/.doctrees/_autosummary/kdrag.datatype.pattern_match.doctree b/.doctrees/_autosummary/kdrag.datatype.pattern_match.doctree
diff --git a/.doctrees/_autosummary/kdrag.doctree b/.doctrees/_autosummary/kdrag.doctree
diff --git a/.doctrees/_autosummary/kdrag.hypothesis.binop.doctree b/.doctrees/_autosummary/kdrag.hypothesis.binop.doctree
diff --git a/.doctrees/_autosummary/kdrag.hypothesis.binops.doctree b/.doctrees/_autosummary/kdrag.hypothesis.binops.doctree
diff --git a/.doctrees/_autosummary/kdrag.hypothesis.compares.doctree b/.doctrees/_autosummary/kdrag.hypothesis.compares.doctree
diff --git a/.doctrees/_autosummary/kdrag.hypothesis.doctree b/.doctrees/_autosummary/kdrag.hypothesis.doctree
diff --git a/.doctrees/_autosummary/kdrag.hypothesis.nitpick.doctree b/.doctrees/_autosummary/kdrag.hypothesis.nitpick.doctree
diff --git a/.doctrees/_autosummary/kdrag.hypothesis.smt_datatype_val.doctree b/.doctrees/_autosummary/kdrag.hypothesis.smt_datatype_val.doctree
diff --git a/.doctrees/_autosummary/kdrag.hypothesis.smt_generic_val.doctree b/.doctrees/_autosummary/kdrag.hypothesis.smt_generic_val.doctree
diff --git a/.doctrees/_autosummary/kdrag.hypothesis.smt_seq_val.doctree b/.doctrees/_autosummary/kdrag.hypothesis.smt_seq_val.doctree
diff --git a/.doctrees/_autosummary/kdrag.hypothesis.sort_occurs.doctree b/.doctrees/_autosummary/kdrag.hypothesis.sort_occurs.doctree
diff --git a/.doctrees/_autosummary/kdrag.hypothesis.val_of_sort.doctree b/.doctrees/_autosummary/kdrag.hypothesis.val_of_sort.doctree
diff --git a/.doctrees/_autosummary/kdrag.hypothesis.z3_array_val.doctree b/.doctrees/_autosummary/kdrag.hypothesis.z3_array_val.doctree
diff --git a/.doctrees/_autosummary/kdrag.kernel.axiom.doctree b/.doctrees/_autosummary/kdrag.kernel.axiom.doctree
diff --git a/.doctrees/_autosummary/kdrag.kernel.beta_conv.doctree b/.doctrees/_autosummary/kdrag.kernel.beta_conv.doctree
diff --git a/.doctrees/_autosummary/kdrag.kernel.consider.doctree b/.doctrees/_autosummary/kdrag.kernel.consider.doctree
diff --git a/.doctrees/_autosummary/kdrag.kernel.define.doctree b/.doctrees/_autosummary/kdrag.kernel.define.doctree
diff --git a/.doctrees/_autosummary/kdrag.kernel.define_fix.doctree b/.doctrees/_autosummary/kdrag.kernel.define_fix.doctree
diff --git a/.doctrees/_autosummary/kdrag.kernel.doctree b/.doctrees/_autosummary/kdrag.kernel.doctree
diff --git a/.doctrees/_autosummary/kdrag.kernel.einstan.doctree b/.doctrees/_autosummary/kdrag.kernel.einstan.doctree
diff --git a/.doctrees/_autosummary/kdrag.kernel.forget.doctree b/.doctrees/_autosummary/kdrag.kernel.forget.doctree
diff --git a/.doctrees/_autosummary/kdrag.kernel.forget2.doctree b/.doctrees/_autosummary/kdrag.kernel.forget2.doctree
diff --git a/.doctrees/_autosummary/kdrag.kernel.fresh_const.doctree b/.doctrees/_autosummary/kdrag.kernel.fresh_const.doctree
diff --git a/.doctrees/_autosummary/kdrag.kernel.herb.doctree b/.doctrees/_autosummary/kdrag.kernel.herb.doctree
diff --git a/.doctrees/_autosummary/kdrag.kernel.instan.doctree b/.doctrees/_autosummary/kdrag.kernel.instan.doctree
diff --git a/.doctrees/_autosummary/kdrag.kernel.instan2.doctree b/.doctrees/_autosummary/kdrag.kernel.instan2.doctree
diff --git a/.doctrees/_autosummary/kdrag.kernel.is_defined.doctree b/.doctrees/_autosummary/kdrag.kernel.is_defined.doctree
diff --git a/.doctrees/_autosummary/kdrag.kernel.is_proof.doctree b/.doctrees/_autosummary/kdrag.kernel.is_proof.doctree
diff --git a/.doctrees/_autosummary/kdrag.kernel.lemma.doctree b/.doctrees/_autosummary/kdrag.kernel.lemma.doctree
diff --git a/.doctrees/_autosummary/kdrag.kernel.skolem.doctree b/.doctrees/_autosummary/kdrag.kernel.skolem.doctree
diff --git a/.doctrees/_autosummary/kdrag.notation.ExistsUnique.doctree b/.doctrees/_autosummary/kdrag.notation.ExistsUnique.doctree
diff --git a/.doctrees/_autosummary/kdrag.notation.QExists.doctree b/.doctrees/_autosummary/kdrag.notation.QExists.doctree
diff --git a/.doctrees/_autosummary/kdrag.notation.QForAll.doctree b/.doctrees/_autosummary/kdrag.notation.QForAll.doctree
diff --git a/.doctrees/_autosummary/kdrag.notation.cond.doctree b/.doctrees/_autosummary/kdrag.notation.cond.doctree
diff --git a/.doctrees/_autosummary/kdrag.notation.conde.doctree b/.doctrees/_autosummary/kdrag.notation.conde.doctree
diff --git a/.doctrees/_autosummary/kdrag.notation.doctree b/.doctrees/_autosummary/kdrag.notation.doctree
diff --git a/.doctrees/_autosummary/kdrag.notation.quantifier_call.doctree b/.doctrees/_autosummary/kdrag.notation.quantifier_call.doctree
diff --git a/.doctrees/_autosummary/kdrag.property.doctree b/.doctrees/_autosummary/kdrag.property.doctree
diff --git a/.doctrees/_autosummary/kdrag.reflect.doctree b/.doctrees/_autosummary/kdrag.reflect.doctree
diff --git a/.doctrees/_autosummary/kdrag.reflect.eval_.doctree b/.doctrees/_autosummary/kdrag.reflect.eval_.doctree
diff --git a/.doctrees/_autosummary/kdrag.reflect.infer_sort.doctree b/.doctrees/_autosummary/kdrag.reflect.infer_sort.doctree
diff --git a/.doctrees/_autosummary/kdrag.reflect.namedtuple_of_constructor.doctree b/.doctrees/_autosummary/kdrag.reflect.namedtuple_of_constructor.doctree
diff --git a/.doctrees/_autosummary/kdrag.reflect.nbe.doctree b/.doctrees/_autosummary/kdrag.reflect.nbe.doctree
diff --git a/.doctrees/_autosummary/kdrag.reflect.reify.doctree b/.doctrees/_autosummary/kdrag.reflect.reify.doctree
diff --git a/.doctrees/_autosummary/kdrag.reflect.sort_of_type.doctree b/.doctrees/_autosummary/kdrag.reflect.sort_of_type.doctree
diff --git a/.doctrees/_autosummary/kdrag.reflect.type_of_sort.doctree b/.doctrees/_autosummary/kdrag.reflect.type_of_sort.doctree
diff --git a/.doctrees/_autosummary/kdrag.rewrite.apply.doctree b/.doctrees/_autosummary/kdrag.rewrite.apply.doctree
diff --git a/.doctrees/_autosummary/kdrag.rewrite.decl_index.doctree b/.doctrees/_autosummary/kdrag.rewrite.decl_index.doctree
diff --git a/.doctrees/_autosummary/kdrag.rewrite.def_eq.doctree b/.doctrees/_autosummary/kdrag.rewrite.def_eq.doctree
diff --git a/.doctrees/_autosummary/kdrag.rewrite.doctree b/.doctrees/_autosummary/kdrag.rewrite.doctree
diff --git a/.doctrees/_autosummary/kdrag.rewrite.horn_of_theorem.doctree b/.doctrees/_autosummary/kdrag.rewrite.horn_of_theorem.doctree
diff --git a/.doctrees/_autosummary/kdrag.rewrite.kbo.doctree b/.doctrees/_autosummary/kdrag.rewrite.kbo.doctree
diff --git a/.doctrees/_autosummary/kdrag.rewrite.lpo.doctree b/.doctrees/_autosummary/kdrag.rewrite.lpo.doctree
diff --git a/.doctrees/_autosummary/kdrag.rewrite.rewrite.doctree b/.doctrees/_autosummary/kdrag.rewrite.rewrite.doctree
diff --git a/.doctrees/_autosummary/kdrag.rewrite.rewrite1.doctree b/.doctrees/_autosummary/kdrag.rewrite.rewrite1.doctree
diff --git a/.doctrees/_autosummary/kdrag.rewrite.rewrite1_rule.doctree b/.doctrees/_autosummary/kdrag.rewrite.rewrite1_rule.doctree
diff --git a/.doctrees/_autosummary/kdrag.rewrite.rewrite_star.doctree b/.doctrees/_autosummary/kdrag.rewrite.rewrite_star.doctree
diff --git a/.doctrees/_autosummary/kdrag.rewrite.rule_of_theorem.doctree b/.doctrees/_autosummary/kdrag.rewrite.rule_of_theorem.doctree
diff --git a/.doctrees/_autosummary/kdrag.rewrite.simp.doctree b/.doctrees/_autosummary/kdrag.rewrite.simp.doctree
diff --git a/.doctrees/_autosummary/kdrag.rewrite.simp1.doctree b/.doctrees/_autosummary/kdrag.rewrite.simp1.doctree
diff --git a/.doctrees/_autosummary/kdrag.rewrite.simp2.doctree b/.doctrees/_autosummary/kdrag.rewrite.simp2.doctree
diff --git a/.doctrees/_autosummary/kdrag.rewrite.unfold.doctree b/.doctrees/_autosummary/kdrag.rewrite.unfold.doctree
diff --git a/.doctrees/_autosummary/kdrag.smt.Eq.doctree b/.doctrees/_autosummary/kdrag.smt.Eq.doctree
diff --git a/.doctrees/_autosummary/kdrag.smt.doctree b/.doctrees/_autosummary/kdrag.smt.doctree
diff --git a/.doctrees/_autosummary/kdrag.smt.is_accessor.doctree b/.doctrees/_autosummary/kdrag.smt.is_accessor.doctree
diff --git a/.doctrees/_autosummary/kdrag.smt.is_constructor.doctree b/.doctrees/_autosummary/kdrag.smt.is_constructor.doctree
diff --git a/.doctrees/_autosummary/kdrag.smt.is_if.doctree b/.doctrees/_autosummary/kdrag.smt.is_if.doctree
diff --git a/.doctrees/_autosummary/kdrag.smt.is_power.doctree b/.doctrees/_autosummary/kdrag.smt.is_power.doctree
diff --git a/.doctrees/_autosummary/kdrag.smt.is_recognizer.doctree b/.doctrees/_autosummary/kdrag.smt.is_recognizer.doctree
diff --git a/.doctrees/_autosummary/kdrag.solvers.aprove.doctree b/.doctrees/_autosummary/kdrag.solvers.aprove.doctree
diff --git a/.doctrees/_autosummary/kdrag.solvers.aprove.run_aprove.doctree b/.doctrees/_autosummary/kdrag.solvers.aprove.run_aprove.doctree
diff --git a/.doctrees/_autosummary/kdrag.solvers.binpath.doctree b/.doctrees/_autosummary/kdrag.solvers.binpath.doctree
diff --git a/.doctrees/_autosummary/kdrag.solvers.collect_decls.doctree b/.doctrees/_autosummary/kdrag.solvers.collect_decls.doctree
diff --git a/.doctrees/_autosummary/kdrag.solvers.collect_sorts.doctree b/.doctrees/_autosummary/kdrag.solvers.collect_sorts.doctree
diff --git a/.doctrees/_autosummary/kdrag.solvers.doctree b/.doctrees/_autosummary/kdrag.solvers.doctree
diff --git a/.doctrees/_autosummary/kdrag.solvers.egglog.doctree b/.doctrees/_autosummary/kdrag.solvers.egglog.doctree
diff --git a/.doctrees/_autosummary/kdrag.solvers.egglog.mangle_name.doctree b/.doctrees/_autosummary/kdrag.solvers.egglog.mangle_name.doctree
diff --git a/.doctrees/_autosummary/kdrag.solvers.egglog.z3_to_egglog.doctree b/.doctrees/_autosummary/kdrag.solvers.egglog.z3_to_egglog.doctree
diff --git a/.doctrees/_autosummary/kdrag.solvers.expr_to_smtlib.doctree b/.doctrees/_autosummary/kdrag.solvers.expr_to_smtlib.doctree
diff --git a/.doctrees/_autosummary/kdrag.solvers.expr_to_tptp.doctree b/.doctrees/_autosummary/kdrag.solvers.expr_to_tptp.doctree
diff --git a/.doctrees/_autosummary/kdrag.solvers.funcdecl_smtlib.doctree b/.doctrees/_autosummary/kdrag.solvers.funcdecl_smtlib.doctree
diff --git a/.doctrees/_autosummary/kdrag.solvers.gappa.doctree b/.doctrees/_autosummary/kdrag.solvers.gappa.doctree
diff --git a/.doctrees/_autosummary/kdrag.solvers.gappa.gappa_of_bool.doctree b/.doctrees/_autosummary/kdrag.solvers.gappa.gappa_of_bool.doctree
diff --git a/.doctrees/_autosummary/kdrag.solvers.gappa.gappa_of_real.doctree b/.doctrees/_autosummary/kdrag.solvers.gappa.gappa_of_real.doctree
diff --git a/.doctrees/_autosummary/kdrag.solvers.install_solvers.doctree b/.doctrees/_autosummary/kdrag.solvers.install_solvers.doctree
diff --git a/.doctrees/_autosummary/kdrag.solvers.mangle_decl.doctree b/.doctrees/_autosummary/kdrag.solvers.mangle_decl.doctree
diff --git a/.doctrees/_autosummary/kdrag.solvers.mangle_decl_smtlib.doctree b/.doctrees/_autosummary/kdrag.solvers.mangle_decl_smtlib.doctree
diff --git a/.doctrees/_autosummary/kdrag.solvers.run.doctree b/.doctrees/_autosummary/kdrag.solvers.run.doctree
diff --git a/.doctrees/_autosummary/kdrag.solvers.smtlib_datatypes.doctree b/.doctrees/_autosummary/kdrag.solvers.smtlib_datatypes.doctree
diff --git a/.doctrees/_autosummary/kdrag.solvers.sort_to_tptp.doctree b/.doctrees/_autosummary/kdrag.solvers.sort_to_tptp.doctree
diff --git a/.doctrees/_autosummary/kdrag.tactics.doctree b/.doctrees/_autosummary/kdrag.tactics.doctree
diff --git a/.doctrees/_autosummary/kdrag.tactics.lemma.doctree b/.doctrees/_autosummary/kdrag.tactics.lemma.doctree
diff --git a/.doctrees/_autosummary/kdrag.tactics.simp.doctree b/.doctrees/_autosummary/kdrag.tactics.simp.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.bitvec.doctree b/.doctrees/_autosummary/kdrag.theories.bitvec.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.doctree b/.doctrees/_autosummary/kdrag.theories.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.float.doctree b/.doctrees/_autosummary/kdrag.theories.float.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.int.doctree b/.doctrees/_autosummary/kdrag.theories.int.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.int.induct.doctree b/.doctrees/_autosummary/kdrag.theories.int.induct.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.int.induct_nat.doctree b/.doctrees/_autosummary/kdrag.theories.int.induct_nat.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.list.Cons.doctree b/.doctrees/_autosummary/kdrag.theories.list.Cons.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.list.List.doctree b/.doctrees/_autosummary/kdrag.theories.list.List.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.list.Nil.doctree b/.doctrees/_autosummary/kdrag.theories.list.Nil.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.list.Unit.doctree b/.doctrees/_autosummary/kdrag.theories.list.Unit.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.list.doctree b/.doctrees/_autosummary/kdrag.theories.list.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.list.list.doctree b/.doctrees/_autosummary/kdrag.theories.list.list.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.nat.doctree b/.doctrees/_autosummary/kdrag.theories.nat.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.option.None_.doctree b/.doctrees/_autosummary/kdrag.theories.option.None_.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.option.Option.doctree b/.doctrees/_autosummary/kdrag.theories.option.Option.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.option.Some.doctree b/.doctrees/_autosummary/kdrag.theories.option.Some.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.option.doctree b/.doctrees/_autosummary/kdrag.theories.option.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.option.get.doctree b/.doctrees/_autosummary/kdrag.theories.option.get.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.option.is_option.doctree b/.doctrees/_autosummary/kdrag.theories.option.is_option.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.real.abstract_arith.doctree b/.doctrees/_autosummary/kdrag.theories.real.abstract_arith.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.real.complex.doctree b/.doctrees/_autosummary/kdrag.theories.real.complex.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.real.doctree b/.doctrees/_autosummary/kdrag.theories.real.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.real.interval.doctree b/.doctrees/_autosummary/kdrag.theories.real.interval.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.real.rlemma.doctree b/.doctrees/_autosummary/kdrag.theories.real.rlemma.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.real.sin_lower.doctree b/.doctrees/_autosummary/kdrag.theories.real.sin_lower.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.real.sqrt_bnd.doctree b/.doctrees/_autosummary/kdrag.theories.real.sqrt_bnd.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.real.sqrt_lower.doctree b/.doctrees/_autosummary/kdrag.theories.real.sqrt_lower.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.real.sqrt_upper.doctree b/.doctrees/_autosummary/kdrag.theories.real.sqrt_upper.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.real.sympy.collect.doctree b/.doctrees/_autosummary/kdrag.theories.real.sympy.collect.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.real.sympy.doctree b/.doctrees/_autosummary/kdrag.theories.real.sympy.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.real.sympy.expand.doctree b/.doctrees/_autosummary/kdrag.theories.real.sympy.expand.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.real.sympy.expand_trig.doctree b/.doctrees/_autosummary/kdrag.theories.real.sympy.expand_trig.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.real.sympy.factor.doctree b/.doctrees/_autosummary/kdrag.theories.real.sympy.factor.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.real.sympy.flint_bnd.doctree b/.doctrees/_autosummary/kdrag.theories.real.sympy.flint_bnd.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.real.sympy.interp_flint.doctree b/.doctrees/_autosummary/kdrag.theories.real.sympy.interp_flint.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.real.sympy.interp_sympy.doctree b/.doctrees/_autosummary/kdrag.theories.real.sympy.interp_sympy.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.real.sympy.simplify.doctree b/.doctrees/_autosummary/kdrag.theories.real.sympy.simplify.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.real.sympy.wrap_sympy.doctree b/.doctrees/_autosummary/kdrag.theories.real.sympy.wrap_sympy.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.real.sympy.z3_of_arb.doctree b/.doctrees/_autosummary/kdrag.theories.real.sympy.z3_of_arb.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.real.sympy.z3_of_sympy.doctree b/.doctrees/_autosummary/kdrag.theories.real.sympy.z3_of_sympy.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.seq.doctree b/.doctrees/_autosummary/kdrag.theories.seq.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.seq.induct.doctree b/.doctrees/_autosummary/kdrag.theories.seq.induct.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.seq.seq.doctree b/.doctrees/_autosummary/kdrag.theories.seq.seq.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.vec.Vec.doctree b/.doctrees/_autosummary/kdrag.theories.vec.Vec.doctree
diff --git a/.doctrees/_autosummary/kdrag.theories.vec.doctree b/.doctrees/_autosummary/kdrag.theories.vec.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.alpha_eq.doctree b/.doctrees/_autosummary/kdrag.utils.alpha_eq.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.ast_size_sexpr.doctree b/.doctrees/_autosummary/kdrag.utils.ast_size_sexpr.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.decls.doctree b/.doctrees/_autosummary/kdrag.utils.decls.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.doctree b/.doctrees/_autosummary/kdrag.utils.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.free_vars.doctree b/.doctrees/_autosummary/kdrag.utils.free_vars.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.generate.doctree b/.doctrees/_autosummary/kdrag.utils.generate.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.is_subterm.doctree b/.doctrees/_autosummary/kdrag.utils.is_subterm.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.is_value.doctree b/.doctrees/_autosummary/kdrag.utils.is_value.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.lemma_db.doctree b/.doctrees/_autosummary/kdrag.utils.lemma_db.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.occurs.doctree b/.doctrees/_autosummary/kdrag.utils.occurs.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.open_binder.doctree b/.doctrees/_autosummary/kdrag.utils.open_binder.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.open_binder_unhygienic.doctree b/.doctrees/_autosummary/kdrag.utils.open_binder_unhygienic.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.pmatch.doctree b/.doctrees/_autosummary/kdrag.utils.pmatch.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.pmatch_rec.doctree b/.doctrees/_autosummary/kdrag.utils.pmatch_rec.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.prompt.doctree b/.doctrees/_autosummary/kdrag.utils.prompt.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.prune.doctree b/.doctrees/_autosummary/kdrag.utils.prune.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.quant_kind_eq.doctree b/.doctrees/_autosummary/kdrag.utils.quant_kind_eq.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.search.doctree b/.doctrees/_autosummary/kdrag.utils.search.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.search_decl.doctree b/.doctrees/_autosummary/kdrag.utils.search_decl.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.search_expr.doctree b/.doctrees/_autosummary/kdrag.utils.search_expr.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.sorts.doctree b/.doctrees/_autosummary/kdrag.utils.sorts.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.subterms.doctree b/.doctrees/_autosummary/kdrag.utils.subterms.doctree
diff --git a/.doctrees/_autosummary/kdrag.utils.unify_db.doctree b/.doctrees/_autosummary/kdrag.utils.unify_db.doctree
diff --git a/.doctrees/environment.pickle b/.doctrees/environment.pickle
diff --git a/.doctrees/index.doctree b/.doctrees/index.doctree
diff --git a/.nojekyll b/.nojekyll
diff --git a/_autosummary/kdrag.all.html b/_autosummary/kdrag.all.html
@@ -0,0 +1,152 @@
+
+
+<!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>kdrag.all &mdash; knuckledragger 0.1 documentation</title>
+      <link rel="stylesheet" type="text/css" href="../_static/pygments.css?v=b86133f3" />
+      <link rel="stylesheet" type="text/css" href="../_static/css/theme.css?v=e59714d7" />
+
+
+      <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=9bcbadda"></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="kdrag.config" href="kdrag.config.html" />
+    <link rel="prev" title="kdrag" href="kdrag.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="kdrag.html">kdrag</a><ul class="current">
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.Calc"><code class="docutils literal notranslate"><span class="pre">Calc</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.Inductive"><code class="docutils literal notranslate"><span class="pre">Inductive()</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.Lemma"><code class="docutils literal notranslate"><span class="pre">Lemma</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.NewType"><code class="docutils literal notranslate"><span class="pre">NewType()</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.QExists"><code class="docutils literal notranslate"><span class="pre">QExists()</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.QForAll"><code class="docutils literal notranslate"><span class="pre">QForAll()</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.Record"><code class="docutils literal notranslate"><span class="pre">Record()</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.axiom"><code class="docutils literal notranslate"><span class="pre">axiom()</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.cond"><code class="docutils literal notranslate"><span class="pre">cond()</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.define"><code class="docutils literal notranslate"><span class="pre">define()</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.lemma"><code class="docutils literal notranslate"><span class="pre">lemma()</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.simp"><code class="docutils literal notranslate"><span class="pre">simp()</span></code></a></li>
+<li class="toctree-l2 current"><a class="current reference internal" href="#">kdrag.all</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.config.html">kdrag.config</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.datatype.html">kdrag.datatype</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.hypothesis.html">kdrag.hypothesis</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.kernel.html">kdrag.kernel</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.notation.html">kdrag.notation</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.property.html">kdrag.property</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.reflect.html">kdrag.reflect</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.rewrite.html">kdrag.rewrite</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.smt.html">kdrag.smt</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.solvers.html">kdrag.solvers</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.tactics.html">kdrag.tactics</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.theories.html">kdrag.theories</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.utils.html">kdrag.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="kdrag.html">kdrag</a></li>
+      <li class="breadcrumb-item active">kdrag.all</li>
+      <li class="wy-breadcrumbs-aside">
+            <a href="../_sources/_autosummary/kdrag.all.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-kdrag.all">
+<span id="kdrag-all"></span><h1>kdrag.all<a class="headerlink" href="#module-kdrag.all" title="Link to this heading"></a></h1>
+<p>A convenience module to import commonly needed other modules as shorthands</p>
+<div class="highlight-python notranslate"><div class="highlight"><pre><span></span><span class="sd">&quot;&quot;&quot;</span>
+<span class="sd">A convenience module to import commonly needed other modules as shorthands</span>
+<span class="sd">&quot;&quot;&quot;</span>
+
+<span class="kn">import</span><span class="w"> </span><span class="nn">kdrag</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="nn">kd</span>
+<span class="kn">import</span><span class="w"> </span><span class="nn">kdrag.smt</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="nn">smt</span>
+
+<span class="c1"># import kdrag.theories.real as real</span>
+<span class="kn">import</span><span class="w"> </span><span class="nn">kdrag.solvers</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="nn">solvers</span>
+<span class="kn">import</span><span class="w"> </span><span class="nn">kdrag.theories.option</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="nn">option</span>
+<span class="kn">import</span><span class="w"> </span><span class="nn">kdrag.theories.list</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="nn">list_</span>
+<span class="kn">import</span><span class="w"> </span><span class="nn">kdrag.theories</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="nn">thy</span>
+</pre></div>
+</div>
+</section>
+
+
+           </div>
+          </div>
+          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
+        <a href="kdrag.html" class="btn btn-neutral float-left" title="kdrag" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
+        <a href="kdrag.config.html" class="btn btn-neutral float-right" title="kdrag.config" 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>
diff --git a/_autosummary/kdrag.config.html b/_autosummary/kdrag.config.html
@@ -0,0 +1,150 @@
+
+
+<!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>kdrag.config &mdash; knuckledragger 0.1 documentation</title>
+      <link rel="stylesheet" type="text/css" href="../_static/pygments.css?v=b86133f3" />
+      <link rel="stylesheet" type="text/css" href="../_static/css/theme.css?v=e59714d7" />
+
+
+      <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=9bcbadda"></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="kdrag.datatype" href="kdrag.datatype.html" />
+    <link rel="prev" title="kdrag.all" href="kdrag.all.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="kdrag.html">kdrag</a><ul class="current">
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.Calc"><code class="docutils literal notranslate"><span class="pre">Calc</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.Inductive"><code class="docutils literal notranslate"><span class="pre">Inductive()</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.Lemma"><code class="docutils literal notranslate"><span class="pre">Lemma</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.NewType"><code class="docutils literal notranslate"><span class="pre">NewType()</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.QExists"><code class="docutils literal notranslate"><span class="pre">QExists()</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.QForAll"><code class="docutils literal notranslate"><span class="pre">QForAll()</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.Record"><code class="docutils literal notranslate"><span class="pre">Record()</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.axiom"><code class="docutils literal notranslate"><span class="pre">axiom()</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.cond"><code class="docutils literal notranslate"><span class="pre">cond()</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.define"><code class="docutils literal notranslate"><span class="pre">define()</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.lemma"><code class="docutils literal notranslate"><span class="pre">lemma()</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.html#kdrag.simp"><code class="docutils literal notranslate"><span class="pre">simp()</span></code></a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.all.html">kdrag.all</a></li>
+<li class="toctree-l2 current"><a class="current reference internal" href="#">kdrag.config</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.datatype.html">kdrag.datatype</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.hypothesis.html">kdrag.hypothesis</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.kernel.html">kdrag.kernel</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.notation.html">kdrag.notation</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.property.html">kdrag.property</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.reflect.html">kdrag.reflect</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.rewrite.html">kdrag.rewrite</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.smt.html">kdrag.smt</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.solvers.html">kdrag.solvers</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.tactics.html">kdrag.tactics</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.theories.html">kdrag.theories</a></li>
+<li class="toctree-l2"><a class="reference internal" href="kdrag.utils.html">kdrag.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="kdrag.html">kdrag</a></li>
+      <li class="breadcrumb-item active">kdrag.config</li>
+      <li class="wy-breadcrumbs-aside">
+            <a href="../_sources/_autosummary/kdrag.config.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-kdrag.config">
+<span id="kdrag-config"></span><h1>kdrag.config<a class="headerlink" href="#module-kdrag.config" title="Link to this heading"></a></h1>
+<p>Global configuration of knuckledragger</p>
+<div class="highlight-python notranslate"><div class="highlight"><pre><span></span><span class="sd">&quot;&quot;&quot;</span>
+<span class="sd">Global configuration of knuckledragger</span>
+<span class="sd">&quot;&quot;&quot;</span>
+
+<span class="n">solver</span> <span class="o">=</span> <span class="kc">None</span>
+<span class="n">admit_enabled</span> <span class="o">=</span> <span class="kc">True</span>
+<span class="c1"># timeout = 1000</span>
+
+<span class="c1"># TODO: Someday, when it is annoyingly slow to check built in theories, we can add a flag to disable them</span>
+<span class="c1"># check_lib = True</span>
+</pre></div>
+</div>
+</section>
+
+
+           </div>
+          </div>
+          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
+        <a href="kdrag.all.html" class="btn btn-neutral float-left" title="kdrag.all" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
+        <a href="kdrag.datatype.html" class="btn btn-neutral float-right" title="kdrag.datatype" 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>