Module pipes 

Which function parameters carry a pipe.

A pipe crosses into a function as a parameter declared by its element type (## To consume (ch: Real): the interpreter types nothing here) or as Pipe of Real. A parameter is a pipe when its function sends into it, receives from it, closes it or selects on it, or hands it to a call or a launch where the callee’s parameter is a pipe. A tier that types a parameter by its declaration asks this first, so a pipe of Real arrives as a pipe, never as a Real.

Functions

declare_pipe_params

The program with every pipe parameter declared as one: ch: Real a pipe parameter becomes ch: Pipe of Real, so each site that types a parameter by its declaration sees the pipe.

pipe_params

The positions of each function’s pipe parameters; a function with none is absent.