elabPartiallyAppliedCoe — Mathlib

Lean4
/-- Elaborator for the `(↑)`, `(⇑)`, and `(↥)` notations. -/
def elabPartiallyAppliedCoe (sym : String) (expectedType : Expr) (mkCoe : (expectedType x : Expr) → TermElabM Expr) :
    TermElabM Expr := do
  let expectedType ← instantiateMVars expectedType
  let Expr.forallE _ a b .. := expectedType |
    do
      tryPostpone
      throwError "({sym }) must have a function type, not{indentExpr expectedType}"
  if b.hasLooseBVars then
    tryPostpone
    throwError "({sym }) must have a non-dependent function type, not{indentExpr expectedType}"
  if a.hasExprMVar then
    tryPostpone
  let f ←
    withLocalDeclD `x a fun x ↦ do
        mkLambdaFVars #[x] (← mkCoe b x)
  return f.etaExpanded?.getD f
Похожие утверждения