Thanks for the quick reply! > Why3 in its current state would not be able to verify the termination of > your 'eval' function, as there is nothing in the contract of 'map' that > promises to only ever apply 'f' to the elements of the list 'l' and > nothing else. In order to verify 'eval' you would essentially need to > inline 'map' into the code of 'eval' (as a local 'let-rec-in' function) > and stay completely first-order.
That's what I did so far, but that's a bit unfortunate. Is there a way to add a specification so that I can use that higher order function or is inlining/duplicating the only far to do it for now? > That said, the error message you've got is not something I would expect > to see here, and we should implement a better error handling for this > case. Could you please submit an issue — just the copy of your email > would suffice. I'd love to open an issue, but I don't have access to the Gitlab instance. If that can be set up somehow I'd happily open an issue! Best regards, Thomas _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
