getDeclTheorems — Mathlib

Lean4
/-- Get candidate theorems from the environment for function property `funPropDecl` and
function `funName`. -/
def getDeclTheorems (funPropDecl : FunPropDecl) (funName : Name) (mainArgs : Array Nat) (appliedArgs : Nat) :
    MetaM (Array FunctionTheorem) := do
  let thms ← getTheoremsForFunction funName funPropDecl.funPropName
  let thms :=
    thms |>.filter (fun thm => (isOrderedSubsetOf mainArgs thm.mainArgs)) |>.qsort
      (fun t s =>
        let dt := (Int.ofNat t.appliedArgs - Int.ofNat appliedArgs).natAbs
        let ds := (Int.ofNat s.appliedArgs - Int.ofNat appliedArgs).natAbs
        match compare dt ds with
        | .lt => true
        | .gt => false
        | .eq => t.mainArgs.size < s.mainArgs.size)
        -- todo: sorting and filtering

  return thms
Похожие утверждения