Lake Targets

This module contains the declarative definition of a Target.

structure Lake.Target (α : Type) : Type

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

• key : BuildKey
• data_def : FamilyDef BuildData self.key α

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

Equations

• Lake.instReprTarget = { reprPrec := Lake.reprTarget✝ }

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

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

Equations

• Lake.instReprTarget_1 = { reprPrec := Lake.Target.repr }

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

Equations

• Lake.instToStringTarget = { toString := fun (x : Lake.Target α) => x.key.toString }

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