- (xdefine ((r r? ...) .. name (a a? ...) ... ) xpr ....)syntax
- (xdefine ((r r? ...) .. #(post name pre) (a a? ...) ... ) xpr ....)syntax
- (xdefine ((r r? ...) .. name (a a? ...) ... as as? ...) xpr ....)syntax
- (xdefine ((r r? ...) .. #(post name pre) (a a? ...) ... as as? ...) xpr ....)syntax
Contract guarded version of define for procedures, where name is the name of the procedure, post and pre document post- and preconditions r ... are return values with corresponding postconditions r? ... a ... are arguments with preconditions a? ... as is a variable collecting rest-parameters with preconditions as? for each such argument, and xpr starts the body..