FStarLang/FStar

F# extraction rely on unsupported features of F#

Opened this issue · 0 comments

I did try to export F* source code to F# and was shown following error messages in .NET 6 and up

F* Code

let center : lens circle point = {
  get = (fun c -> c.center);
  put = (fun n c -> {c with center = n})
}

produce extraction error like this

error FS0062: This construct is deprecated. The use of multiple parenthesized type parameters before a generic type name such as '( 
int, int) Map' was deprecated in F# 2.0 and is no longer supported. You can enable this feature by using '--langversion:5.0' and '--mlcompatibility'.

Also export add #light “off” to the beginning of the file which is no longer supported and produces error.

There workarounds for this, but if extraction left as is, it would eventually stagnate and break one day or another.