Module reduce 

Applies a reduction function on records grouped by key.

The reduce operator acts on (key, val) data. Records with the same key are grouped together, and a user-supplied reduction function is applied to the key and the list of values. The function is expected to populate a list of output values.

The output can change at times that are joins of input times, not only at input times themselves, and the operator must determine at which times to re-evaluate the reduction. A machine-checked account of which times suffice lives in formal/Differential/Coverage.lean.

Traits

ReduceTactic

A type that resolves a key-wise reduction over batches arriving on the input.

Functions

reduce_trace

A key-wise reduction of values in an input trace.

reduce_with_tactic

Drives a key-wise reduction using a supplied ReduceTactic.