Home

Awesome

This mode is now unmaitained and has fallen behind the development of F*

FStar Interactive Mode

An interactive mode for type-checking F* code, built as a package for the Atom editor. Package was originally adapted from atom-build.

Installation

Usage

In a F* buffer, pressing Ctrl+Shift+I will place a marker in the file and type-check the file from the previous marker (the start of the file, if there isn't one) until the current cursor.

Ctrl+Alt+G will jump to the next error, if any.

Ctrl+Alt+A will display all the errors.

Ctrl+Alt+C will kill the running background F* process. It's useful to do this to reset your state in case you observe odd behaviors.

Ctrl+Shift+N will type-check the file until the first (* check_marker *) comment (or to the current cursor, like Ctrl+Shift+I, in case there is no such marker).

Key bindings are platform-dependent: See the F* Interactive menu under Packages in Atom.