pre- and post-conditions

4.18: adda/cstr/function/pre- and post-conditions:
. we need a syntax that extends a function's type expression
to include the function's pre- and post-conditions
which are predicates that reduce the function's space
by testing both the input and output for certain conditions .
. math syntax sometimes uses the (|) operator for such work .
. perhaps the new syntax for a function type literal could be:
(x.t).t | (pre-condition; post-condition) .