[PVS-Help] Nested LET and implicit types

[Johannes Eriksson <joheriks@xxxxxx>]

Hello,

what are the mechanisms in PVS that enable the following theory to be
accepted by the type checker (without TCCs):

test_let: theory begin
	T1,T2: type+
    t1: T1
    t2: T2
    f: [T1->bool]

    l1: lemma f(t1) = (let z=t1 in (let z=t2 in f(z)))
    l2: lemma f(t1) = (let z=t2 in f(z)) where z=t1
end test_let

The following messages are generated:

Added existence AXIOM for T1:
T1_nonempty: AXIOM EXISTS (x: T1): TRUE;

Added existence AXIOM for T2:
T2_nonempty: AXIOM EXISTS (x: T2): TRUE;

LET/WHERE variable z at line 7, col 27 is given type
  T1 from its value expression.

LET/WHERE variable z at line 7, col 40 is given type
  T2 from its value expression.

LET/WHERE variable z at line 8, col 47 is given type
  T1 from its value expression.

LET/WHERE variable z at line 8, col 27 is given type
  T2 from its value expression.


The lemmas are provable. I was expecting it to generate a type
error. The inner let, which is type incorrect, seems to be "skipped
over" somehow by the type checker.  Why?

Regards,
Johannes
-- 
Johannes W. E. Eriksson, M.Sc.
Ph.D. Student / Turku Centre For Computer Science (TUCS)
Åbo Akademi University / Department of Information Technologies
e-mail: joheriks@abo.fi  www: http://www.abo.fi/~joheriks