[SMT-LIB] overloading and type checking.

[Tjark Weber]

On Thu, 2010-11-04 at 07:54 +0000, cok at frontiernet.net wrote:
> - if we are to have overloading by return type and the 'as' construct,
> I'd rather it be limited to constants

There are, of course, motivating examples that are not constants -- in
fact, any function whose return type is not uniquely determined by its
argument types.

For instance, consider the sum type (i.e., the tagged union) (Sum X Y),
with injections

  inl (X) (Sum X Y)   and   inr (Y) (Sum X Y).

Regards,
Tjark