Improve define's return-specs to support lazy hints

[ragerdl]

Putting the request here, in case someone gets the inkling to implement it.

It'd be good to be able to type:

(define address-fix
  ((address address-p))
  :returns (retval ubyte32p :enable (address-p))
  ...)

instead of:

(define address-fix
  ((address address-p))
  :returns (retval ubyte32p :hints (("goal" :in-theory (enable address-p))))
  ...)

An implementation of this feature request should also support the other keywords that define supports, like :disable. It may turn out that it doesn't make sense to support them all.

[acoglio]

I suppose that this could be realized by integrating return type specifiers with defrule, which supports "direct" keyword hints — :enable, :disable, :use, etc.