The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

On Thu, Apr 30, 2015 at 10:53 AM Randy Pollack <rpollack0 AT gmail.com> wrote:

Thanks Guillaume, that was informative.

> Casts have no computational meaning, they are just meant as hints
> (and even then, the type checker tends to ignore them unless they ask
>  for a specific reduction machinery, so they are basically just hints for
> the pretyper).

Then why isn't casting removed from the typechecked terms in my example?

Because it can be useful to inform the kernel which conversion algorithm you want. The kernel type checker does not ignore casts in this sense, it implements the rule I gave, so it has some computational meaning for conversion (not reduction): you'll get different performance from the different conversion algorithms used to check conversion of the infered and ascribed types.

Best,

-- Matthieu