302def pointwiseBinary =
303 (lambda erased word : Type 0 .
304 (lambda erased inputs : Nat .
305 (lambda unrestricted operation : (family PointwiseBinary) .
306 (lambda unrestricted left : (family PointwiseExpression word inputs) .
307 (lambda unrestricted right : (family PointwiseExpression word inputs) .
308 (constructor
309 PointwiseExpression
310 PointwiseBinaryExpression
311 word
312 inputs
313 operation
314 left
315 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.