Translate types of the Gospelstdlib

ocaml-gospel / ortac

Runtime assertion checking based on Gospel specifications

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

MIT License

38 stars 10 forks source link

Translate types of the Gospelstdlib #158

Closed shym closed 1 year ago

shym commented 1 year ago

Add a tystdlib to the Context, similar to the stdlib but for types Use tystdlib in Ocaml_of_gospel functions translating types Adapt QCheck-STM to feed the context to those translation functions Add a new test for QCheck-STM using the sequence type for the model

Closes #155

shym commented 1 year ago

Thank you! I agree with the proposed improvement, and even dropped the fold_X_namespace specialized functions altogether.