def Lean.LocalContext.inaccessibleFVars (lctx : LocalContext) : Array 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.

def Lean.Meta.getInaccessibleFVars {m : Type → Type} [Monad m] [MonadLCtx m] : m (Array 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 __do_lift.inaccessibleFVars

def Lean.MVarId.renameInaccessibleFVars (mvarId : MVarId) : MetaM (MVarId × Array 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.