Sut as type argument or inside tuple

ocaml-gospel / ortac

Runtime assertion checking based on Gospel specifications

https://ocaml-gospel.github.io/ortac/

MIT License

38 stars 10 forks source link

Closed nikolaushuber closed 3 months ago

nikolaushuber commented 3 months ago

Fixes a bug were we are not checking for the sut type being used as the instantiation of a type variable or inside a tuple, so for example

val test : 'a t list -> int
(*@ r = test ts
    ensures r = List.length ts *)

would type check correctly and create incorrect code.