Re: [Hol-info] Learning HOL Light

[<rd...@le...>]

>    Just because you don't write the A doesn't mean it isn't there. And
>    if you'll still need to be careful if there's an A in context,
>    whether you write it explicitly or not, although hopefully type
>    inference will pick another type variable for you if there's
>    already an A around (e.g. B).
>
> Thanks, Ramana!  I think type inference always behaves that way. I mean,
> I've always assumed it did, and in my limited experience, it does.
>
>

I believe the type checkers in all known HOL implementations are designed
to give you the most general possible typing subject to any explicit type
constraints. So where Ramana said "hopefully", I would say "unless there's
a bug".

Regards,

Rob.