Documentation

Lake.Config.Opaque

source
instance Lake.OpaqueWorkspace.instNonempty :
Nonempty OpaqueWorkspace
source
def Lake.OpaqueWorkspace :
Type

Opaque reference to a Workspace used for forward declaration.

Equations
    Instances For
      source
      def Lake.OpaqueTargetConfig (pkgName name : Lean.Name) :
      Type

      Opaque reference to a TargetConfig used for forward declaration.

      Equations
        Instances For
          source
          instance Lake.OpaqueTargetConfig.instNonempty {pkgName name : Lean.Name} :
          Nonempty (OpaqueTargetConfig pkgName name)