Nicolas Osborne

> Regarding the place for redefining the Shrink module, do you have a preference of either putting it in the runtime or in the generated code? IMO it's probably a...

@nikolaushuber will you be willing / have time to resume working on this PR ? (If no, I can update it and merge it for the next release). Also, I'm...

Thanks! I'll rebase the PR and see if there is any update to do.

Thanks! I believe the problem comes from [here](https://github.com/ocaml-gospel/ortac/blob/main/plugins/qcheck-stm/src/ir_of_gospel.ml#L175) Gospel sometimes add an `fs_apply` symbol in the AST that is not handle here.

Thanks for raising this issue! There are in fact two problems here. Regarding the `bool` type, Gospel is transforming equality between terms of type `prop` into a double equivalence. Meaning:...

Thanks you and well spotted! After a quick look, it appears we don't even collect this piece of information (whether it is a named or an optional argument) in the...

Yes it is :-). Ortac captures the Gospel errors and displays them with the `Gospel error:` prefix. What is happening here, it that `f` is asking for an `int` but...