Nick Battle
Nick Battle
Ah, I see what you mean. Interesting. But in general it's quite a tricky thing to infer - there is an arbitrary expression involving possibly multiple variables in the binding,...
Interesting. I hadn't come across Limes notation, though it is only mentioned in German web pages - do you just mean limit notation? You might be on to something here....
It would certainly be possible to create an annotation, but what functionality would it have - is there a proof obligation associated with the limit?
But if an empty sequence was passed to the example expression, the body of the forall expression would never be evaluated, so it would be fine. The problem is that...
There's a small bug that is causing the warning to be suppressed in VDMJ/Overture (the inds typecheck is not propagating the emptiness of its argument to the emptiness of its...
Incidentally, the same kind of error occurs with empty maps ("Empty map cannot be applied" errors) that are inside some sort of conditional defence. The search for an uncomplicated way...
Looking at the VDMJ code (and I assume Overture is the same), the argument types are only checked if the apply expression is of a function, not an operation. I...
I have a patch for this, but it produces some unusual side effects. Need to look into it more closely before committing.
Is it the same with VDMJ? I'm on holiday at the moment, but will look at this when I get back.
OK, now back from holiday. I think I can see what's happening. It's because you have "let a, b in set ...". For the duplicated tests, both a and b...