Declaration parameters example not working as expected

[kai-e]

I've tried to cargo-cult the declaration parameter example (groups) from the PVS 6.0 release notes to define monotone functions:

mon_gen: THEORY
BEGIN
  T[U: TYPE+]: TYPE+ FROM U
  poT[U: TYPE+]: TYPE = (partial_order?[T[U]])
  monontone?[S, D: TYPE+](leqS: poT[S], leqT: poT[D])(f: [T[S] -> T[D]]): bool =
    FORALL(s1, s1: T[S]): leqS(s1, s2) IMPLIES leqT(f(s1), f(s2))
END mon_gen

This parses but doesn't typecheck. The error is

Break: maybe-instantiate-from-decl-formals*

which is the same error I get when running the typchecker over the groups example. This could be just a documentation bug or a regression in PVS 7.1.

[samowre]

Hi Kai,

Thanks for reporting this, I'll look into is shortly and get back to you.

Regards, Sam

Kai @.***> wrote:

I've tried to cargo-cult the declaration parameter example (groups) from the PVS 6.0 release notes to define monotone functions:

mon_gen: THEORY BEGIN T[U: TYPE+]: TYPE+ FROM U poT[U: TYPE+]: TYPE = (partial_order?[T[U]]) monontone?[S, D: TYPE+](leqS: poT[S], leqT: poT[D])(f: [T[S] -> T[D]]): bool = FORALL(s1, s1: T[S]): leqS(s1, s2) IMPLIES leqT(f(s1), f(s2)) END mon_gen

This parses but doesn't typecheck. The error is

Break: maybe-instantiate-from-decl-formals*

which is the same error I get when running the typchecker over the groups example. This could be just a documentation bug or a regression in PVS 7.1.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe.