Re: [isabelle-dev] »real« considered harmful

[Lars Noschinski]

On 24.06.2015 16:29, Larry Paulson wrote:
> This may be the problem. I don’t remember exactly what I was trying to do, 
> only that it was very difficult. Of course nobody uses show_types any more.
At least this was the problem for me. A notorious instance of the same
problem are the functions in HOL-Word, e.g. "ucast :: 'a word => 'b
word" and "uint :: 'a word => int". Getting at the types of things like
"uint (ucast 4)" in some big term happens often when verifying C
programs and is pretty annoying. Such things need a disambiguating
output syntax (at least as long as hovering in the output buffer doesn't
show the types, maybe even then).
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev