Index

_

__contains__() (kdrag.rewrite.Order class method) __getitem__() (kdrag.rewrite.Order class method)

__iter__() (kdrag.rewrite.Order class method) __len__() (kdrag.rewrite.Order class method)

A

a (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) abstract_arith() (in module kdrag.theories.real), [1] accessor_lemmas() (in module kdrag.datatype), [1] accessor_num() (in module kdrag.datatype), [1] add (in module kdrag.notation) add() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.SATSolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method) add_note() (kdrag.kernel.LemmaError method) (kdrag.rewrite.RewriteRuleException method) admit (kdrag.kernel.Proof attribute) (kdrag.Proof attribute)

admit() (kdrag.Lemma method) (kdrag.tactics.Lemma method) alpha_eq() (in module kdrag.utils), [1] and_ (in module kdrag.notation) apply() (in module kdrag.rewrite), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) args (kdrag.kernel.Defn attribute) (kdrag.kernel.LemmaError attribute) (kdrag.rewrite.RewriteRuleException attribute) assert_and_track() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method) assumption() (kdrag.Lemma method) (kdrag.tactics.Lemma method) ast_size_sexpr() (in module kdrag.utils), [1] auto() (kdrag.Lemma method) (kdrag.tactics.Lemma method) ax (kdrag.kernel.Defn attribute) axiom() (in module kdrag) (in module kdrag.kernel), [1]

B

b (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute)

BaseSolver (class in kdrag.solvers) beta_conv() (in module kdrag.kernel), [1] binop() (in module kdrag.hypothesis), [1] binops() (in module kdrag.hypothesis), [1] binpath() (in module kdrag.solvers), [1] body (kdrag.kernel.Defn attribute) bound() (kdrag.solvers.gappa.GappaSolver method) BVTheory (class in kdrag.theories.bitvec)

C

c (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) Calc (class in kdrag) (class in kdrag.tactics) cases() (kdrag.Lemma method) (kdrag.tactics.Lemma method) check() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.SATSolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method) check_tptp_status() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method)

clear() (kdrag.Lemma method) (kdrag.tactics.Lemma method) collect_decls() (in module kdrag.solvers), [1] collect_sorts() (in module kdrag.solvers), [1] compares() (in module kdrag.hypothesis), [1] conc (kdrag.rewrite.Rule attribute) Cond (class in kdrag.notation) cond() (in module kdrag) (in module kdrag.notation), [1] conde() (in module kdrag.notation), [1] Cons() (in module kdrag.theories.list), [1] consider() (in module kdrag.kernel), [1] constructor_num() (in module kdrag.datatype), [1] copy() (kdrag.Lemma method) (kdrag.tactics.Lemma method) count() (kdrag.rewrite.RewriteRule method) (kdrag.rewrite.Rule method) (kdrag.tactics.Goal method) ctx (kdrag.tactics.Goal attribute)

D

datatype_call() (in module kdrag.datatype), [1] datatype_iter() (in module kdrag.datatype), [1] datatype_len() (in module kdrag.datatype), [1] datatype_match_() (in module kdrag.datatype), [1] datatype_replace() (in module kdrag.datatype), [1] decl_index() (in module kdrag.rewrite), [1] decls() (in module kdrag.utils), [1] def_eq() (in module kdrag.rewrite), [1] define() (in module kdrag) (in module kdrag.kernel), [1] (kdrag.notation.SortDispatch method)

define_fix() (in module kdrag.kernel), [1] Defn (class in kdrag.kernel) defns (in module kdrag.kernel) diff() (in module kdrag.theories.real.sympy), [1] (in module kdrag.theories.set), [1] distinct_lemmas() (in module kdrag.datatype), [1] div (in module kdrag.notation)

E

EgglogSolver (class in kdrag.solvers.egglog) einstan() (in module kdrag.kernel), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) empty() (kdrag.tactics.Goal class method) Enum() (in module kdrag.datatype), [1] EProverTHFSolver (class in kdrag.solvers) EQ (kdrag.rewrite.Order attribute) Eq() (in module kdrag.smt), [1] eq() (kdrag.Calc method) (kdrag.Lemma method) (kdrag.tactics.Calc method) (kdrag.tactics.Lemma method)

eval_() (in module kdrag.reflect), [1] exists() (kdrag.Lemma method) (kdrag.tactics.Lemma method) ExistsUnique() (in module kdrag.notation), [1] expand() (in module kdrag.theories.real.sympy), [1] expr() (kdrag.notation.Cond method) expr_to_smtlib() (in module kdrag.solvers), [1] expr_to_tptp() (in module kdrag.solvers), [1] ext() (kdrag.Lemma method) (kdrag.tactics.Lemma method) extract() (kdrag.solvers.egglog.EgglogSolver method)

F

factor() (in module kdrag.theories.real.sympy), [1] fix() (kdrag.Lemma method) (kdrag.tactics.Lemma method) fixes() (kdrag.Lemma method) (kdrag.tactics.Lemma method)

flint_bnd() (in module kdrag.theories.real.sympy), [1] forget() (in module kdrag.kernel), [1] forget2() (in module kdrag.kernel), [1] free_vars() (in module kdrag.utils), [1] fresh_const() (in module kdrag.kernel), [1] funcdecl_smtlib() (in module kdrag.solvers), [1]

G

gappa_of_bool() (in module kdrag.solvers.gappa), [1] gappa_of_real() (in module kdrag.solvers.gappa), [1] GappaSolver (class in kdrag.solvers.gappa) ge (in module kdrag.notation) ge() (kdrag.Calc method) (kdrag.tactics.Calc method) generalize() (kdrag.Lemma method) (kdrag.tactics.Lemma method) generate() (in module kdrag.utils), [1] GenericProof (class in kdrag.property)

get() (in module kdrag.theories.option), [1] (kdrag.property.GenericProof method) getitem (in module kdrag.notation) globals (kdrag.reflect.KnuckleClosure attribute) Goal (class in kdrag.tactics) goal (kdrag.tactics.Goal attribute) GR (kdrag.rewrite.Order attribute) gt (in module kdrag.notation) gt() (kdrag.Calc method) (kdrag.tactics.Calc method)

H

have() (kdrag.Lemma method) (kdrag.tactics.Lemma method)

herb() (in module kdrag.kernel), [1] horn_of_theorem() (in module kdrag.rewrite), [1] hyp (kdrag.rewrite.Rule attribute)

I

index() (kdrag.rewrite.RewriteRule method) (kdrag.rewrite.Rule method) (kdrag.tactics.Goal method) induct (in module kdrag.notation) induct() (in module kdrag.theories.int), [1] (in module kdrag.theories.seq), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) induct_inductive() (in module kdrag.kernel), [1] induct_nat() (in module kdrag.theories.int), [1] Inductive() (in module kdrag) (in module kdrag.kernel), [1] InductiveRel() (in module kdrag.datatype), [1] infer_sort() (in module kdrag.reflect), [1] inj_lemmas() (in module kdrag.datatype), [1] install_solvers() (in module kdrag.solvers), [1] instan() (in module kdrag.kernel), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method)

instan2() (in module kdrag.kernel), [1] integrate() (in module kdrag.theories.real.sympy), [1] inter() (in module kdrag.theories.set), [1] interp_flint() (in module kdrag.theories.real.sympy), [1] intros() (kdrag.Lemma method) (kdrag.tactics.Lemma method) invert (in module kdrag.notation) is_accessor() (in module kdrag.smt), [1] is_constructor() (in module kdrag.smt), [1] is_defined() (in module kdrag.kernel), [1] is_empty() (kdrag.tactics.Goal method) is_if() (in module kdrag.smt), [1] is_option() (in module kdrag.theories.option), [1] is_power() (in module kdrag.smt), [1] is_proof() (in module kdrag.kernel), [1] is_recognizer() (in module kdrag.smt), [1] is_subterm() (in module kdrag.utils), [1] is_uninterp() (in module kdrag.smt), [1] is_value() (in module kdrag.utils), [1]

K

k (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) kbo() (in module kdrag.rewrite), [1] kdify() (in module kdrag.theories.real.sympy), [1] kdrag module kdrag.all module kdrag.config module kdrag.datatype module kdrag.hypothesis module kdrag.kernel module kdrag.notation module kdrag.property module kdrag.reflect module kdrag.rewrite module kdrag.smt module kdrag.solvers module kdrag.solvers.aprove module

kdrag.solvers.egglog module kdrag.solvers.gappa module kdrag.tactics module kdrag.theories module kdrag.theories.bitvec module kdrag.theories.float module kdrag.theories.fun module kdrag.theories.int module kdrag.theories.list module kdrag.theories.nat module kdrag.theories.option module kdrag.theories.real module kdrag.theories.real.complex module kdrag.theories.real.interval module kdrag.theories.real.sympy module kdrag.theories.seq module kdrag.theories.set module kdrag.theories.vec module kdrag.utils module KnuckleClosure (class in kdrag.reflect)

L

lam (kdrag.reflect.KnuckleClosure attribute) le (in module kdrag.notation) le() (kdrag.Calc method) (kdrag.tactics.Calc method) left() (kdrag.Lemma method) (kdrag.tactics.Lemma method) Lemma (class in kdrag) (class in kdrag.tactics) lemma() (kdrag.property.GenericProof method) lemma_db() (in module kdrag.utils), [1] LemmaError

length_empty (kdrag.theories.seq.Seq attribute) LeoIIISolver (class in kdrag.solvers) let() (kdrag.solvers.egglog.EgglogSolver method) lhs (kdrag.rewrite.RewriteRule attribute) limit() (in module kdrag.theories.real.sympy), [1] List() (in module kdrag.theories.list), [1] list() (in module kdrag.theories.list), [1] locals (kdrag.reflect.KnuckleClosure attribute) lpo() (in module kdrag.rewrite), [1] lt (in module kdrag.notation) lt() (kdrag.Calc method) (kdrag.tactics.Calc method)

M

m (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) mangle_decl() (in module kdrag.solvers), [1] mangle_decl_smtlib() (in module kdrag.solvers), [1] mangle_name() (in module kdrag.solvers.egglog), [1] matmul (in module kdrag.notation) member() (in module kdrag.theories.set), [1] module kdrag kdrag.all kdrag.config kdrag.datatype kdrag.hypothesis kdrag.kernel kdrag.notation kdrag.property kdrag.reflect kdrag.rewrite kdrag.smt kdrag.solvers kdrag.solvers.aprove kdrag.solvers.egglog kdrag.solvers.gappa kdrag.tactics kdrag.theories kdrag.theories.bitvec kdrag.theories.float kdrag.theories.fun kdrag.theories.int kdrag.theories.list kdrag.theories.nat kdrag.theories.option kdrag.theories.real kdrag.theories.real.complex kdrag.theories.real.interval kdrag.theories.real.sympy kdrag.theories.seq kdrag.theories.set kdrag.theories.vec kdrag.utils

mul (in module kdrag.notation) multipattern_match() (in module kdrag.datatype), [1] MultiSolver (class in kdrag.solvers)

N

n (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) name (kdrag.kernel.Defn attribute)

namedtuple_of_constructor() (in module kdrag.reflect), [1] NanoCopISolver (class in kdrag.solvers) nbe() (in module kdrag.reflect), [1] neg (in module kdrag.notation) newgoal() (kdrag.Lemma method) (kdrag.tactics.Lemma method) NewType() (in module kdrag) (in module kdrag.datatype), [1] NGE (kdrag.rewrite.Order attribute) Nil() (in module kdrag.theories.list), [1] nitpick() (in module kdrag.hypothesis), [1] None_() (in module kdrag.theories.option), [1]

O

occurs() (in module kdrag.utils), [1] open_binder() (in module kdrag.utils), [1] open_binder_unhygienic() (in module kdrag.utils), [1]

Option() (in module kdrag.theories.option), [1] or_ (in module kdrag.notation) Order (class in kdrag.rewrite) otherwise() (kdrag.notation.Cond method)

P

pattern_match() (in module kdrag.datatype), [1] pf (kdrag.rewrite.Rule attribute) pmatch() (in module kdrag.utils), [1] pmatch_rec() (in module kdrag.utils), [1] pop() (kdrag.Lemma method) (kdrag.tactics.Lemma method) predefined (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) predefined_names (kdrag.solvers.egglog.EgglogSolver attribute) predefined_sorts (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute)

prompt() (in module kdrag.utils), [1] Proof (class in kdrag) (class in kdrag.kernel) proof() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method) prove() (in module kdrag) (in module kdrag.kernel), [1] (in module kdrag.tactics), [1] prune() (in module kdrag.utils), [1] push() (kdrag.Lemma method) (kdrag.tactics.Lemma method)

Q

qed() (kdrag.Calc method) (kdrag.Lemma method) (kdrag.tactics.Calc method) (kdrag.tactics.Lemma method) QExists() (in module kdrag) (in module kdrag.notation), [1]

QForAll() (in module kdrag) (in module kdrag.notation), [1] quant_kind_eq() (in module kdrag.utils), [1] quantifier_call() (in module kdrag.notation), [1] query() (kdrag.solvers.VampireSolver method)

R

radd (in module kdrag.notation) reason (kdrag.kernel.Proof attribute) (kdrag.Proof attribute) recognizer_lemmas() (in module kdrag.datatype), [1] register() (kdrag.notation.SortDispatch method) (kdrag.property.GenericProof method) reify() (in module kdrag.reflect), [1] rel (in module kdrag.datatype) replace_rational_with_ratval() (in module kdrag.theories.real.sympy), [1] res (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) rewrite() (in module kdrag.rewrite), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method)

rewrite1() (in module kdrag.rewrite), [1] rewrite1_rule() (in module kdrag.rewrite), [1] rewrite_star() (in module kdrag.rewrite), [1] RewriteRule (class in kdrag.rewrite) RewriteRuleException rhs (kdrag.rewrite.RewriteRule attribute) right() (kdrag.Lemma method) (kdrag.tactics.Lemma method) rlemma() (in module kdrag.theories.real), [1] rmul (in module kdrag.notation) Rule (class in kdrag.rewrite) rule_of_theorem() (in module kdrag.rewrite), [1] run() (in module kdrag.solvers), [1] (kdrag.solvers.egglog.EgglogSolver method) run_aprove() (in module kdrag.solvers.aprove), [1] run_cmd() (kdrag.solvers.egglog.EgglogSolver method) rw() (kdrag.Lemma method) (kdrag.tactics.Lemma method)

S

SATSolver (class in kdrag.solvers) search() (in module kdrag) (in module kdrag.utils), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) search_decl() (in module kdrag.utils), [1] search_expr() (in module kdrag.utils), [1] Seq (class in kdrag.theories.seq) seq() (in module kdrag.theories.seq), [1] series() (in module kdrag.theories.real.sympy), [1] Set() (in module kdrag.theories.set), [1] set() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method) show() (kdrag.Lemma method) (kdrag.tactics.Lemma method) sig (kdrag.tactics.Goal attribute) simp() (in module kdrag) (in module kdrag.rewrite), [1] (in module kdrag.tactics), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method)

simp1() (in module kdrag.rewrite), [1] simp2() (in module kdrag.rewrite), [1] simp_tac() (in module kdrag.tactics), [1] simplify() (in module kdrag.theories.real.sympy), [1] sin_lower() (in module kdrag.theories.real), [1] skolem() (in module kdrag.kernel), [1] smt_datatype_val() (in module kdrag.hypothesis), [1] smt_generic_val() (in module kdrag.hypothesis), [1] smt_seq_val() (in module kdrag.hypothesis), [1] smtlib_datatypes() (in module kdrag.solvers), [1] solver_classes (kdrag.solvers.MultiSolver attribute) Some() (in module kdrag.theories.option), [1] sort_occurs() (in module kdrag.hypothesis), [1] sort_of_type() (in module kdrag.reflect), [1] sort_to_tptp() (in module kdrag.solvers), [1] SortDispatch (class in kdrag.notation) sorts() (in module kdrag.utils), [1] split() (kdrag.Lemma method) (kdrag.tactics.Lemma method) sqrt_bnd() (in module kdrag.theories.real), [1] sqrt_lower() (in module kdrag.theories.real), [1] sqrt_upper() (in module kdrag.theories.real), [1] Struct() (in module kdrag) (in module kdrag.datatype), [1] sub (in module kdrag.notation) subset() (in module kdrag.theories.set), [1] subterms() (in module kdrag.utils), [1] summation() (in module kdrag.theories.real.sympy), [1] symm() (kdrag.Lemma method) (kdrag.tactics.Lemma method) sympify() (in module kdrag.theories.real.sympy), [1]

T

then() (kdrag.notation.Cond method) thm (kdrag.kernel.Proof attribute) (kdrag.Proof attribute) top_goal() (kdrag.Lemma method) (kdrag.tactics.Lemma method)

translate_tuple_args() (in module kdrag.theories.real.sympy), [1] TweeSolver (class in kdrag.solvers) type_of_sort() (in module kdrag.reflect), [1]

U

unfold() (in module kdrag.rewrite), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) unify_db() (in module kdrag.utils), [1] union() (in module kdrag.theories.set), [1] Unit() (in module kdrag.theories.list), [1] unsat_core() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method)

V

val_of_sort() (in module kdrag.hypothesis), [1] VampireSolver (class in kdrag.solvers) VampireTHFSolver (class in kdrag.solvers)

Vec() (in module kdrag.theories.vec), [1] VecTheory (class in kdrag.theories.vec) vs (kdrag.rewrite.RewriteRule attribute) (kdrag.rewrite.Rule attribute)

W

wf (in module kdrag.notation) when() (kdrag.notation.Cond method) with_traceback() (kdrag.kernel.LemmaError method) (kdrag.rewrite.RewriteRuleException method) write_smt() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method)

write_tptp() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method)

X

x (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute)

Y

y (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute)

Z

z (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute)

z3_array_val() (in module kdrag.hypothesis), [1] z3_of_arb() (in module kdrag.theories.real.sympy), [1] z3_to_egglog() (in module kdrag.solvers.egglog), [1] ZipperpositionSolver (class in kdrag.solvers)