mn200/HOL — Issue #39: Provide good indication of all constants’ real name and type
Author: mn200
Created: 2011-10-11 05:01:48+00:00
State: open

show_types works tolerably well for indicating the types of variables and some constants. But when a constant is involved in a special syntactic form (typically an infix) or is overloaded polymorphically, the user gets nothing back at all. For example,

- load "integerTheory";
- show_types := true;
- ``x + y``;
> val it = ``(x: int) + (y:int)`` : term

No indication that `+` is really `int$+`, though it's easy enough (given knowledge about the theories) to see that this is so. With `show_types` on,

- ``LENGTH``;
> val it = ``(LENGTH : α list -> num)`` : term

(good). But also:

- Define`SUC (n:int) = n + 1`;
> val it = |- ∀(n :int). SUC n = n + (1 :int) : thm

(bad) and

- ``SUC``;
<>
> val it = ``SUC`` : term

(also bad).

For the last example, I'd like to see

``SUC : int -> int``

as this case isn't.

Worse, I'm not sure what the output should be in the following scenario. Just annotating the `SUC` with its type is not sufficient:

- Define`SUC (n:num) = n - 1`;
Definition has been stored under "SUC_def"
> val it =
|- ∀(n :num). SUC n = n − (1 :num) : thm

- ``SUC x``;
<>
> val it = ``SUC (x :num)`` : term

- dest_term (rator it);
> val it =
CONST
{Ty = ``:num -> num``,
Thy = "scratch", Name = "SUC"} : lambda