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

PVS Bug 1057


Synopsis:        show-expanded-form does not expand measure
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Thu Jun 10 10:35:01 -0700 2010
Originator:      Hendrik Tews
Release:         PVS 4.2
Organization:    os.inf.tu-dresden.de
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  C-u M-x show-expanded-form does not give the theory name of the
  measure relation. For instance in the following theory:
  
      A : Theory
      Begin
        f(l : list[nat]) : RECURSIVE bool = true
        Measure l by <<
      End A
  
  
  Bye,
  
  Hendrik

How-To-Repeat: 

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