AlphaGitHub
Source/Packages

Component.Pointwise

packages/components/src/Component/Pointwise.alpha

413 lines45 declarations17.7 KiBSHA-256 d94b209ac952
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 289–293

pointwiseSlotsSeparate

Full file
Logical slot identities are independent of their eventual physical layout. Learner compositions use this relation to keep writable state separate from observations; the target planner separately owns physical non-overlap.
289def pointwiseSlotsSeparate =
290  (lambda erased slots : Nat .
291    (lambda unrestricted left : (family StdFin slots) .
292      (lambda unrestricted right : (family StdFin slots) .
293        (naturalIsZero (naturalEqual (stdFinToNatural slots left) (stdFinToNatural slots right))))))

The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.