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
rewrite1()
kdrag.utils.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.rewrite1
View page source
kdrag.utils.rewrite1
kdrag.utils.
rewrite1
(
t
:
ExprRef
,
vs
:
list
[
ExprRef
]
,
lhs
:
ExprRef
,
rhs
:
ExprRef
)
→
ExprRef
|
None
Rewrite at root a single time.