structure Lake.ConfigTarget (kind : Lean.Name) : Type

A user-configured target -- its package and its configuration. This is the general structure from which LeanLib, LeanExe, etc. are derived.

• pkg : Package

  The package the target belongs to.

• name : Lean.Name

  The target's name.

• config : ConfigType kind self.pkg.name self.name

  The target's user-defined configuration.

instance Lake.instHashableConfigTarget {k : Lean.Name} : Hashable (ConfigTarget k)

instance Lake.instBEqConfigTarget {k : Lean.Name} : BEq (ConfigTarget k)

@[simp]

axiom Lake.OpaqueConfigTarget.def {k : Lean.Name} : OpaqueConfigTarget k = ConfigTarget k

@[inline]

def Lake.PConfigDecl.mkConfigTarget (pkg : Package) (self : PConfigDecl pkg.name) : ConfigTarget self.kind

@[inline]

def Lake.Package.configTargets (kind : Lean.Name) (self : Package) : Array (ConfigTarget kind)

Returns the package targets of the specified kind (as an Array).

@[inline]

def Lake.Package.findConfigTarget? (kind name : Lean.Name) (self : Package) : Option (ConfigTarget kind)

Try to find a package target of the given name and kind.