def
HammerCore.hammerCoreSingleRuleTac
(formulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × String))
(includeLCtx : Bool)
(configOptions : ConfigurationOptions)
:
Constructs a SingleRuleTac that uses Lean-auto/Zipperposition to attempt to solve the input goal with formulas (and all facts in the local context
if includeLCtx is enabled), and either throws an error (if Lean-auto/Zipperposition fail) or suggests a Duper invocation using the subset of formulas
that Zipperposition used to find a proof.
TODO Currently, Zipperposition's unsat core is not used to minimize the set of formulas from the local context that are sent to Duper, but in the future, this behavior should be added as an option (it should theoretically improve the strength of some suggested Duper invocations at the cost of increasing the size of all suggested Duper invocations).
Equations
- One or more equations did not get rendered due to their size.