|The snippet below reproduces mysterious behaviour in a bigger project|
tup_small : THEORY
ARR [T: TYPE]: TYPE =
[# size : nat
, content : [below(size) -> T]
TUP [T: TYPE] : TYPE = [T, nat]
valid_bag? [T: TYPE] (a: ARR[TUP]): bool =
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?