setupLCtx

Mathlib.Util.Notation3

URI: https://scilib.ai/kg/mathlib#Mathlib.Notation3.setupLCtx

Lean4

/-- Adds all the names in `boundNames` to the local context
with types that are fresh metavariables.
This is used for example when initializing `p` in `(scoped p => ...)` when elaborating `...`. -/
def setupLCtx (lctx : LocalContext) (boundNames : Array Name) : MetaM (LocalContext × Std.HashMap FVarId Name) := do
  let mut lctx := lctx
  let mut boundFVars := { }
  for name in boundNames do
    let fvarId ← mkFreshFVarId
    lctx := lctx.mkLocalDecl fvarId name (← withLCtx lctx (← getLocalInstances) mkFreshTypeMVar)
    boundFVars := boundFVars.insert fvarId name
  return (lctx, boundFVars)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru