Index

A

abstract_arith() (in module kdrag.theories.real) alpha_eq() (in module kdrag.utils)

apply() (in module kdrag.utils) axiom() (in module kdrag.kernel)

B

beta_conv() (in module kdrag.kernel)

binpath() (in module kdrag.solvers)

C

collect() (in module kdrag.theories.real.sympy) collect_decls() (in module kdrag.solvers)

collect_sorts() (in module kdrag.solvers) cond() (in module kdrag.notation) consider() (in module kdrag.kernel)

D

datatype_call() (in module kdrag.notation) decl_index() (in module kdrag.utils)

decls() (in module kdrag.utils) define() (in module kdrag.kernel) define_fix() (in module kdrag.kernel)

E

ExistsUnique() (in module kdrag.notation) expand() (in module kdrag.theories.real.sympy) expand_trig() (in module kdrag.theories.real.sympy)

expr_to_lean() (in module kdrag.utils) expr_to_smtlib() (in module kdrag.solvers) expr_to_tptp() (in module kdrag.solvers)

F

factor() (in module kdrag.theories.real.sympy) FinSort() (in module kdrag.theories.vec) flint_bnd() (in module kdrag.theories.real.sympy)

forget() (in module kdrag.kernel) forget2() (in module kdrag.kernel) fresh_const() (in module kdrag.kernel) funcdecl_smtlib() (in module kdrag.solvers)

G

gappa_of_bool() (in module kdrag.solvers.gappa)

gappa_of_real() (in module kdrag.solvers.gappa) generate() (in module kdrag.utils)

H

herb() (in module kdrag.kernel)

horn_of_theorem() (in module kdrag.utils)

I

induct() (in module kdrag.theories.datatypes) (in module kdrag.theories.datatypes.nat) (in module kdrag.theories.seq) induct_nat() (in module kdrag.theories.int) install_solvers() (in module kdrag.solvers)

instan() (in module kdrag.kernel) instan2() (in module kdrag.kernel) interp_flint() (in module kdrag.theories.real.sympy) interp_sympy() (in module kdrag.theories.real.sympy) is_proof() (in module kdrag.kernel) is_value() (in module kdrag.utils)

K

kdrag module kdrag.all module kdrag.config module kdrag.kernel module kdrag.notation module kdrag.smt module kdrag.solvers module kdrag.solvers.egglog module kdrag.solvers.gappa module kdrag.tactics module kdrag.theories module

kdrag.theories.bitvec module kdrag.theories.complex module kdrag.theories.datatypes module kdrag.theories.datatypes.nat module kdrag.theories.int module kdrag.theories.interval module kdrag.theories.real module kdrag.theories.real.sympy module kdrag.theories.seq module kdrag.theories.vec module kdrag.utils module

L

lemma() (in module kdrag.kernel) (in module kdrag.tactics)

lemma_db() (in module kdrag.utils)

M

mangle_decl() (in module kdrag.solvers) mangle_name() (in module kdrag.solvers.egglog) module kdrag kdrag.all kdrag.config kdrag.kernel kdrag.notation kdrag.smt kdrag.solvers kdrag.solvers.egglog kdrag.solvers.gappa kdrag.tactics kdrag.theories kdrag.theories.bitvec kdrag.theories.complex kdrag.theories.datatypes kdrag.theories.datatypes.nat kdrag.theories.int kdrag.theories.interval kdrag.theories.real kdrag.theories.real.sympy kdrag.theories.seq kdrag.theories.vec kdrag.utils

N

NewType() (in module kdrag.notation)

O

occurs() (in module kdrag.utils)

open_binder() (in module kdrag.utils)

P

pmatch() (in module kdrag.utils)

prompt() (in module kdrag.utils)

Q

QExists() (in module kdrag.notation)

QForAll() (in module kdrag.notation) quant_kind_eq() (in module kdrag.utils)

R

Record() (in module kdrag.notation) rewrite() (in module kdrag.utils) rewrite1() (in module kdrag.utils)

rewrite_star() (in module kdrag.utils) rlemma() (in module kdrag.theories.real) rule_of_theorem() (in module kdrag.utils) run() (in module kdrag.solvers)

S

simp() (in module kdrag.tactics) (in module kdrag.utils) simp2() (in module kdrag.utils) simplify() (in module kdrag.theories.real.sympy) sin_lower() (in module kdrag.theories.real) skolem() (in module kdrag.kernel)

smtlib_datatypes() (in module kdrag.solvers) sort_to_tptp() (in module kdrag.solvers) sorts() (in module kdrag.utils) sqrt_bnd() (in module kdrag.theories.real) sqrt_lower() (in module kdrag.theories.real) sqrt_upper() (in module kdrag.theories.real) subterms() (in module kdrag.utils)

U

unify_db() (in module kdrag.utils)

V

Vec() (in module kdrag.theories.vec)

W

wrap_sympy() (in module kdrag.theories.real.sympy)

Z

z3_of_arb() (in module kdrag.theories.real.sympy)

z3_of_sympy() (in module kdrag.theories.real.sympy) z3_to_egglog() (in module kdrag.solvers.egglog)