# PVS Bug 737

Synopsis: show-expanded-sequent does not show instanciations of all infix operators
Severity: serious
Priority: medium
Responsible: owre (Sam Owre)
State: analyzed
Class: sw-bug
Arrival-Date: Mon Feb 3 11:50:02 2003
Originator: Hendrik Tews
Organization: tcs.inf.tu-dresden.de
Release: PVS 3.0
Environment:
System:
Architecture:
Description:
Hi,
consider the following theory
T : Theory
Begin
n : Var nat
f(n) : nat = n + 1
g(n) : nat = n + 2
h(n) : nat = n + 2
a : Lemma f o g = h
end T
If I invoke a proof on lemma a, expand f and invoke then M-x
show-expanded-sequent I get
a :
|-------
{1} function_props[nat, nat, nat].O(LAMBDA (n): 1 + n, g) = h
So show-expanded-sequent shows me the instanciation for "o", but
not for "+" and neither for "=".
(BTW. the "o" is wronly capitalized.)
Why are these infix operators handled differently?
What can I do to get the theory and instanciation of the other
infix operators?
IMHO show-expanded-sequent
should show the theory and instanciation of all constants (and
thus of all infix operators).
Bye,
Hendrik
How-To-Repeat:
Fix:
Made the obvious fixes.