FStar icon indicating copy to clipboard operation
FStar copied to clipboard

Invalid OCaml extracted when using `{ record with update }` syntax for dependent types with exactly one data constructor

Open chandradeepdey opened this issue 1 year ago • 0 comments

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 avatar Apr 20 '24 19:04 chandradeepdey