FStar
FStar copied to clipboard
Invalid OCaml extracted when using `{ record with update }` syntax for dependent types with exactly one data constructor
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