Documentation

Batteries.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.

Equations
  • One or more equations did not get rendered due to their size.
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.

    Equations
    • Lean.Meta.getInaccessibleFVars = do let __do_liftLean.getLCtx pure __do_lift.inaccessibleFVars
    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.

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