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

[PVS-Help] Type checking issue



The snippet below reproduces mysterious behaviour in a bigger project

===
tup_small : THEORY

  BEGIN

  ARR [T: TYPE]: TYPE =
  [# size    : nat
   , content : [below(size) -> T]
   #]

  TUP [T: TYPE] : TYPE = [T, nat]
  
  valid_bag? [T: TYPE] (a: ARR[TUP]): bool =
    TRUE

  END tup_small
===

When trying to type check, I get at the bottom a message that says SPC-Scroll, I-ignore etc.

There is also an Error:assertion report at the top.

I am wondering what I did wrong? 

Thanks,

Jonathan