3 ms·
according to the tutorial "F* provides a facility to specify interfaces to external modules that are implemented elsewhere. For example, operations that perform
by platz 11y ago
according to the tutorial "F* provides a facility to specify interfaces to external modules that are implemented elsewhere. For example, operations that perform file input/output are implemented by the operating system and made available to F* programs via the underlying framework, e.g., .NET or OCaml."
- platz 11y agoit looks like they are able to reference mscorlib https://github.com/FStarLang/FStar/blob/997b1f20f35142e650325da7054a37f425ad1b00/old/to_be_ported/sep/prims-sep.fst#L188 https://github.com/FStarLang/FStar/blob/997b1f20f35142e65032... and F# with these externs https://github.com/FStarLang/FStar/blob/997b1f20f35142e650325da7054a37f425ad1b00/old/to_be_ported/pldi10-benchmarks/lookout/externs.fine#L8 https://github.com/FStarLang/FStar/blob/997b1f20f35142e65032...
- jaked89 11y agoThis code exists in a folder named "old/to_be_ported", which might indicate that it no longer functions. It appears that the correct way is to create a .fsi file. A few examples: https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba221b1f354216218cd397/lib/system.fsi https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba... https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba221b1f354216218cd397/lib/system.diagnostics.fsi https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba... https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba221b1f354216218cd397/lib/system.text.fsi https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba... https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba221b1f354216218cd397/lib/system.collections.generic.fsi https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba... https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba221b1f354216218cd397/lib/system.io.fsi https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba...
- platz 11y agoahh, good catch