Documentation

Std.Lean.Meta.Inaccessible

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.

Instances For

    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.

    Instances For

      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.

      Instances For