Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

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.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools