knuckledragger
kdrag
kdrag.all
kdrag.config
kdrag.kernel
kdrag.notation
kdrag.smt
kdrag.solvers
kdrag.tactics
kdrag.theories
kdrag.utils
kdrag.utils.alpha_eq
kdrag.utils.apply
kdrag.utils.decl_index
kdrag.utils.decls
kdrag.utils.expr_to_lean
kdrag.utils.generate
kdrag.utils.horn_of_theorem
kdrag.utils.is_value
kdrag.utils.lemma_db
kdrag.utils.occurs
kdrag.utils.open_binder
kdrag.utils.pmatch
kdrag.utils.prompt
kdrag.utils.quant_kind_eq
kdrag.utils.rewrite
kdrag.utils.rewrite1
kdrag.utils.rewrite_star
kdrag.utils.rule_of_theorem
rule_of_theorem()
kdrag.utils.simp
kdrag.utils.simp2
kdrag.utils.sorts
kdrag.utils.subterms
kdrag.utils.unify_db
knuckledragger
kdrag
kdrag.utils
kdrag.utils.rule_of_theorem
View page source
kdrag.utils.rule_of_theorem
kdrag.utils.
rule_of_theorem
(
thm
:
BoolRef
)
→
Rule
Unpack theorem of form
forall vs, lhs = rhs
into a Rule tuple