[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Typechecking confused by a LET expression?

Hi PVS experts,

the attached example fails to type check, but I do not understand why.
It seems that the typechecker is somehow confused by a LET expression
(see comments in file).

Can you help?

Piotr Trojanek

Attachment: foo.pvs
Description: Binary data