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

• Lake.instBEqConfigTarget
• Lake.instHashableConfigTarget

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

Equations

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

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

Equations

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

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

Equations

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

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

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