ink

def Lean.LocalContext.inaccessibleFVars (lctx : Lean.LocalContext) : Array Lean.LocalDecl

Obtain the inaccessible fvars from the given local context. An fvar is inaccessible if (a) its user name is inaccessible or (b) it is shadowed by a later fvar with the same user name.

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Meta.getInaccessibleFVars {m : Type → Type} [inst : Monad m] [inst : Lean.MonadLCtx m] : m (Array Lean.LocalDecl)

Obtain the inaccessible fvars from the current local context. An fvar is inaccessible if (a) its user name is inaccessible or (b) it is shadowed by a later fvar with the same user name.

Equations

• Lean.Meta.getInaccessibleFVars = do let __do_lift ← Lean.getLCtx pure (Lean.LocalContext.inaccessibleFVars __do_lift)

ink

def Lean.MVarId.renameInaccessibleFVars (mvarId : Lean.MVarId) : Lean.MetaM (Lean.MVarId × Array Lean.FVarId)

Rename all inaccessible fvars. An fvar is inaccessible if (a) its user name is inaccessible or (b) it is shadowed by a later fvar with the same user name. This function gives all inaccessible fvars a unique, accessible user name. It returns the new goal and the fvars that were renamed.

Equations

• One or more equations did not get rendered due to their size.