Documentation

Lake.Build.Target.Basic

Lake Targets #

This module contains the declarative definition of a Target.

structure Lake.Target (α : Type) :

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

Instances For
    def Lake.Target.repr {α : Type} (x : Target α) (prec : Nat) :
    Equations
    Instances For
      instance Lake.instReprTarget {α : Type} :
      Equations
      Equations
      @[reducible, inline]
      abbrev Lake.TargetArray (α : Type) :

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

      Equations
      Instances For