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
kdrag.utils.simp
kdrag.utils.simp2
kdrag.utils.sorts
kdrag.utils.subterms
kdrag.utils.unify_db
unify_db()
knuckledragger
kdrag
kdrag.utils
kdrag.utils.unify_db
View page source
kdrag.utils.unify_db
kdrag.utils.
unify_db
(
p1
:
ExprRef
,
p2
:
ExprRef
)
→
dict
[
ExprRef
,
ExprRef
]
|
None
Unification using de Bruijn indices as variables