Lake Targets

This module contains the declarative definition of a Target.

structure Lake.Target (α : Type) : Type

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

• key : PartialBuildKey

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

instance Lake.instReprTarget {α : Type} : Repr (Target α)

instance Lake.instToStringTarget {α : Type} : ToString (Target α)

instance Lake.instCoePartialBuildKeyTarget {α : Type} : Coe PartialBuildKey (Target α)

@[reducible, inline]

abbrev Lake.TargetArray (α : Type) : Type

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