def Lake.BuildKey.fetch {α : Type} (self : BuildKey) [h : FamilyOut BuildData self α] : FetchM (Job α)

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lake.Target.fetch {α : Type} (self : Target α) : FetchM (Job α)

Equations

• self.fetch = self.key.fetch

def Lake.TargetArray.fetch {α : Type} (self : TargetArray α) : FetchM (Job (Array α))

Equations

• self.fetch = Lake.Job.collectArray <$> Array.mapM (fun (x : Lake.Target α) => x.fetch) self