Forbid `old` operator in precondition clauses (`requires` and `checks`) - Githubissues

ocaml-gospel / gospel

A tool-agnostic formal specification language for OCaml.

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

MIT License

126 stars 16 forks source link

Forbid `old` operator in precondition clauses (`requires` and `checks`) #335

Closed n-osborne closed 12 months ago

n-osborne commented 12 months ago

Route whereami information in type checker
Reject old in requires and checks clauses

n-osborne commented 12 months ago

CI is happy. I merge.