This 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/4e4162f736195b2031ba...

https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba...

https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba...

https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba...

https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba...