Every input `expression` reads is shared or of class `allowed`.
559def dataParallelReadsClass =
560 (lambda unrestricted slots : Nat .
561 (lambda unrestricted k : Nat .
562 (lambda unrestricted m : Nat .
563 (lambda unrestricted q : Nat .
564 (lambda unrestricted allowed : Nat .
565 (lambda unrestricted expression : (family PointwiseExpression StdU64 slots) .
566 (pointwiseFold
567 StdU64
568 Nat
569 slots
570 (lambda unrestricted operation : (family PointwiseUnary) .
571 (lambda unrestricted child : Nat . child))
572 (lambda unrestricted operation : (family PointwiseBinary) .
573 (lambda unrestricted left : Nat .
574 (lambda unrestricted right : Nat . (naturalAnd left right))))
575 (lambda unrestricted word : StdU64 . 1)
576 expression
577 (lambda unrestricted index : (family StdFin slots) .
578 (let unrestricted class =
579 (dataParallelSlotClass k m q (stdFinToNatural slots index))
580 in
581 (naturalOr (naturalIsZero class) (naturalEqual class allowed)))))))))))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.