Documentation

Lake.Config.Glob

inductive Lake.Glob :

A specification of a set of module names.

Instances For
    partial def Lake.forEachModuleIn {m : TypeType u_1} [Monad m] [MonadLiftT IO m] (dir : Lake.FilePath) (f : Lake.Namem PUnit) (ext : optParam String "lean") :
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[inline]
      def Lake.Glob.forEachModuleIn {m : TypeType u_1} [Monad m] [MonadLiftT IO m] (dir : Lake.FilePath) (f : Lake.Namem PUnit) (self : Lake.Glob) :
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For