Read-only observations may alias each other; they must not alias the state
being mutated. The same independent-slot obligation used by scaled-gradient
compositions prevents a placement from silently changing the local rule.
36def scaledProductAssignments =
37 (lambda erased word : Type 0 .
38 (lambda erased slots : Nat .
39 (lambda unrestricted state : (family StdFin slots) .
40 (lambda unrestricted coefficient : (family StdFin slots) .
41 (lambda unrestricted left : (family StdFin slots) .
42 (lambda unrestricted right : (family StdFin slots) .
43 (lambda erased independent : (equal Nat (scaledProductSlotsIndependent slots state coefficient left right) 1) .
44 (let unrestricted input =
45 (lambda unrestricted index : (family StdFin slots) .
46 (constructor PointwiseExpression PointwiseInput word slots index))
47 in
48 (constructor
49 StdList
50 StdListCons
51 (family PointwiseAssignment word slots)
52 (constructor
53 PointwiseAssignment
54 PointwiseAssign
55 word
56 slots
57 state
58 (accumulateScaledProduct
59 (family PointwiseExpression word slots)
60 (pointwiseBinary word slots (constructor PointwiseBinary PointwiseAdd))
61 (pointwiseBinary word slots (constructor PointwiseBinary PointwiseMultiply))
62 (input coefficient)
63 (input state)
64 (input left)
65 (input right)))
66 (constructor StdList StdListEmpty (family PointwiseAssignment word slots)))))))))))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.