mkContext? — Mathlib

Lean4
/-- Populate a `context` object for evaluating `e`. -/
def mkContext? (e : Expr) : MetaM (Option Context) := do
  let e ← instantiateMVars e
  let type ← instantiateMVars <| ← inferType e
  match (← whnfR type).getAppFnArgs with
  | (``Quiver.Hom, #[_, _, f, _]) =>
    let C ← instantiateMVars <| ← inferType f
    let .succ level₁ ← getLevel C |
      return none
    let .succ level₂ ← getLevel type |
      return none
    let some instCat ← synthInstance? (mkAppN (.const ``Category [level₂, level₁]) #[C]) |
      return none
    let instMonoidal? ← synthInstance? (mkAppN (.const ``MonoidalCategory [level₂, level₁]) #[C, instCat])
    return some ⟨level₂, level₁, C, instCat, instMonoidal?⟩
  | _ =>
    return none
Похожие утверждения