def Lean.PremiseSelection.orElse (s₁ : Selector) (s₂ : Unit → Selector) : Selector

Try the first premise selector. If it throws an error, try the second one.

Equations

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

instance Lean.PremiseSelection.instOrElseSelector_premiseSelection : OrElse Selector

Equations

• Lean.PremiseSelection.instOrElseSelector_premiseSelection = { orElse := Lean.PremiseSelection.orElse }

def Lean.PremiseSelection.interleave (selectors : Array Selector) : Selector

A single combinator that lets each of the n selectors select k premises, merge the n * k results by rank, and returns the deduplicated top k among them.

This combinator is inspired by MeSh, but it is a simplified version of MeSh. (MeSh can control the weight and steepness of probability density for each selector.)

Equations

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