# Lake Targets #

This module contains the declarative definition of a `Target`.

source
structure Lake.Target (α : Type) :
Type

A Lake target that is expected to produce an output of a specific type.

- key : PartialBuildKey

Instances For

source
@[reducible, inline]
abbrev Lake.TargetArray (α : Type) :
Type

Shorthand for `Array (Target α)` that supports dot notation for Lake-specific operations (e.g., `fetch`).

Equations

- Lake.TargetArray α = Array (Lake.Target α)

Instances For

source
def Lake.Target.repr {α : Type} (x : Target α) (prec : Nat) :
Std.Format
Equations

- x.repr prec = Repr.addAppParen (Std.Format.nest (if prec ≥ 1024 then 1 else 2) (Std.Format.text "Lake.Target.mk" ++ Std.Format.line ++ reprArg x.key)).group prec

Instances For

source
instance Lake.Target.instRepr {α : Type} :
Repr (Target α)
Equations

- Lake.Target.instRepr = { reprPrec := Lake.Target.repr }

source
instance Lake.Target.instToString {α : Type} :
ToString (Target α)
Equations

- Lake.Target.instToString = { toString := fun (x : Lake.Target α) => x.key.toString }

source
instance Lake.Target.instCoePartialBuildKey {α : Type} :
Coe PartialBuildKey (Target α)
Equations

- Lake.Target.instCoePartialBuildKey = { coe := Lake.Target.mk }