instance Lake.OpaqueWorkspace.instNonempty : Nonempty OpaqueWorkspace

def Lake.OpaqueWorkspace : Type

Opaque reference to a Workspace used for forward declaration.

Equations

• Lake.OpaqueWorkspace = Lake.OpaqueWorkspace.nonemptyType✝.type

def Lake.OpaqueTargetConfig (pkgName name : Lean.Name) : Type

Opaque reference to a TargetConfig used for forward declaration.

Equations

• Lake.OpaqueTargetConfig pkgName name = (Lake.OpaqueTargetConfig.nonemptyType✝ pkgName name).type

instance Lake.OpaqueTargetConfig.instNonempty {pkgName name : Lean.Name} : Nonempty (OpaqueTargetConfig pkgName name)