isMorApplication — Mathlib

Lean4
/-- Is function body of `f` a morphism application? What kind? -/
def isMorApplication (f : FunctionData) : MetaM MorApplication := do
  if let some name := f.fn.constName? then
    if ← Mor.isCoeFunName name then
      let info ← getConstInfo name
      let arity := info.type.getNumHeadForalls
      match compare arity f.args.size with
      | .eq =>
        return .exact
      | .lt =>
        return .overApplied
      | .gt =>
        return .underApplied
  match h : f.args.size with
  | 0 =>
    return .none
  | n + 1 =>
    if f.args[n].coe.isSome then
      return .exact
    else if f.args.any (fun a => a.coe.isSome) then
      return .overApplied
    else
      return .none
Похожие утверждения