source
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.

Instances For

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

- Lake.instHashableConfigTarget = { hash := fun (x : Lake.ConfigTarget k) => hash x.name }

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

- Lake.instBEqConfigTarget = { beq := fun (x1 x2 : Lake.ConfigTarget k) => x1.name == x2.name }

source
@[simp]
axiom Lake.OpaqueConfigTarget.def {k : Lean.Name} :
OpaqueConfigTarget k = ConfigTarget k
source
@[inline]
def Lake.PConfigDecl.mkConfigTarget (pkg : Package) (self : PConfigDecl pkg.name) :
ConfigTarget self.kind
Equations

- Lake.PConfigDecl.mkConfigTarget pkg self = { pkg := pkg, name := self.name, config := self.config' }

Instances For

source
@[inline]
def Lake.Package.configTargets (kind : Lean.Name) (self : Package) :
Array (ConfigTarget kind)

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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.

Equations

- One or more equations did not get rendered due to their size.

Instances For