MePo premise selection

This is a naive implement of the MePo premise selection algorithm, from "Lightweight relevance filtering for machine-generated resolution problems" by Meng and Paulson.

It needs to be tuned and evaluated for Lean.

def Lean.PremiseSelection.mepoSelector (useRarity : Bool) (p : Float := 0.6) (c : Float := 2.4) : Selector

Equations

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