opaque Lake.OpaquePackage.nonemptyType : NonemptyType

instance Lake.instNonemptyOpaquePackage : Nonempty Lake.OpaquePackage

Equations

• Lake.instNonemptyOpaquePackage = ⋯

def Lake.OpaquePackage : Type

Opaque reference to a Package used for forward declaration.

Equations

• Lake.OpaquePackage = Lake.OpaquePackage.nonemptyType.type

def Lake.OpaqueWorkspace : Type

Opaque reference to a Workspace used for forward declaration.

Equations

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

opaque Lake.OpaqueWorkspace.nonemptyType : NonemptyType

instance Lake.instNonemptyOpaqueWorkspace : Nonempty Lake.OpaqueWorkspace

Equations

• Lake.instNonemptyOpaqueWorkspace = ⋯

opaque Lake.OpaqueTargetConfig.nonemptyType {Name : Sort u_1} (pkgName : Name) (name : Name) : NonemptyType

instance Lake.instNonemptyOpaqueTargetConfig : ∀ {Name : Sort u_1} {pkgName name : Name}, Nonempty (Lake.OpaqueTargetConfig pkgName name)

Equations

• ⋯ = ⋯

def Lake.OpaqueTargetConfig {Name : Sort u_1} (pkgName : Name) (name : Name) : Type

Opaque reference to a TargetConfig used for forward declaration.

Equations

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