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

[PVS-Help] abbreviating theories with assuming sections



With PVS version 4.2, type-checking the following spec gives me this error

  "Theory ex has no formal parameters, hence no need for ASSUMING section"

specific : THEORY
BEGIN
  T : TYPE;
  f : [T -> T];
  e : T;
END specific

general [T : TYPE, f : [T -> T], e : T] : THEORY
BEGIN
  ASSUMING
    idem : ASSUMPTION f(e) = e;
  ENDASSUMING
END general

x : THEORY
BEGIN
  IMPORTING specific
  ex : THEORY = general[specific.T, specific.f, specific.e];
END x

This seems to mean that it's always a type-check error to abbreviate a
theory with an ASSUMING part. That doesn't seem like it should cause a
type error.

Thanks.