Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Invalid OCaml extracted when using { record with update } syntax for inductive types with exactly one data constructor #3258

Open
chandradeepdey opened this issue Apr 20, 2024 · 0 comments

Comments

@chandradeepdey
Copy link
Contributor

module Test

type foo = | Foo : m: int -> n: int{n > m} -> foo

let bar (f: foo) : foo = { f with n = f.n + 1 }

The F* code works, but the extracted OCaml code misses a comma and parentheses

@chandradeepdey chandradeepdey changed the title Invalid OCaml extracted when using { record with update } syntax for normal types with exactly one data constructor Invalid OCaml extracted when using { record with update } syntax for inductive types with exactly one data constructor Apr 20, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant