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
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
knuckledragger
kdrag
kdrag.utils
kdrag.utils.open_binder
View page source
kdrag.utils.open_binder
kdrag.utils.
open_binder
(
lam
:
QuantifierRef
)
→
tuple
[
list
[
ExprRef
]
,
ExprRef
]
Open a quantifier with fresh variables