# PVS Bug 508

Synopsis: pretty printer captures constants
Severity: serious
Priority: medium
Responsible: dave_sc (Dave Stringer-Calvert)
State: analyzed
Class: sw-bug
Arrival-Date: Mon Jan 8 10:40:01 2001
Originator: Hendrik Tews
Organization: inf.tu-dresden.de
Release: PVS 2.3
Environment:
System:
Architecture:
Description:
Hi,
Consider the following theory:
A : Theory
Begin
f(n : nat) : nat = 1
a : Lemma
(Lambda(h : [nat -> nat]) : Forall(f : [nat -> nat]) : h = f) (f)
end A
invoke a proof on a and do assert, this yields
a :
|-------
{1} FORALL (f: [nat -> nat]): f = f
In this sequent the bound variable f and the constant f are mixed
up. Internally they are still different (as (expand "f")
demonstrates).
I consider the capture of the constant a bug, because the printed
sequent is a tautology, whereas the internal version is false. At
least the output of M-x show-expanded-sequent should be in 1-1
correspondence with the internal representation.
Bye,
Hendrik
How-To-Repeat:
Fix:
Fixed substit to check for capture of a constant.