def HammerCore.containsConst (e : Lean.Expr) (p : Lean.Name → Bool) : Bool

Returns true if e contains a name n where p n is true. Copied from Mathlib.Lean.Expr.Basic.lean

Equations

• HammerCore.containsConst e p = (Lean.Expr.find? (fun (x : Lean.Expr) => match x with | Lean.Expr.const n us => p n | x => false) e).isSome

def HammerCore.unsatCoreIncludesFact (unsatCoreDerivLeafStrings : Array String) (fact : Lean.Term) : Bool

Checks unsatCoreDerivLeafStrings to see if it contains a string that matches fact.

Equations

• One or more equations did not get rendered due to their size.

def HammerCore.unsatCoreIncludesFactAsString (unsatCoreDerivLeafStrings : Array String) (fact : String) : Bool

Like unsatCoreIncludesFact but takes fact as a String instead of a Term.

Equations

• One or more equations did not get rendered due to their size.

def HammerCore.getDuperCoreLemmas (unsatCoreDerivLeafStrings : Array String) (userFacts : Lean.Syntax.TSepArray `term ",") (goalDecls : Array Lean.LocalDecl) (includeAllLctx : Bool) (duperConfigOptions : Duper.ConfigurationOptions) : Lean.Elab.Tactic.TacticM (Array Lean.Term × Lean.Expr)

Uses unsatCoreDerivLeafStrings to filter userFacts to only include facts that appear in the external prover's unsat core, then passes just those facts to Duper to reconstruct the proof in Lean.

Equations

• One or more equations did not get rendered due to their size.