- >> x loc .. x? ...procedure
postcondition test: passes x unchanged only if all predicates x? return #t on it raises a result-exception at location loc, if given, or '>> otherwise
postcondition test: passes x unchanged only if all predicates x? return #t on it raises a result-exception at location loc, if given, or '>> otherwise