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 (← inferType e)).getAppFnArgs with
  | (``Quiver.Hom, #[_, _, f, _]) =>
    let fType ← instantiateMVars <| ← inferType f
    match (← whnfR fType).getAppFnArgs with
    | (``Quiver.Hom, #[_, _, a, _]) =>
      let B ← inferType a
      let .succ level₀ ← getLevel B |
        return none
      let .succ level₁ ← getLevel fType |
        return none
      let .succ level₂ ← getLevel type |
        return none
      let some instBicategory ← synthInstance? (mkAppN (.const ``Bicategory [level₂, level₁, level₀]) #[B]) |
        return none
      return some ⟨level₂, level₁, level₀, B, instBicategory⟩
    | _ =>
      return none
  | _ =>
    return none
Похожие утверждения