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
rewrite_star()
kdrag.utils.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.rewrite_star
View page source
kdrag.utils.rewrite_star
kdrag.utils.
rewrite_star
(
t
:
ExprRef
,
rules
:
list
[
Rule
]
)
→
ExprRef
Repeat rewrite until no more rewrites are possible.