:lang fstar

(dependent) types and (monadic) effects and Z3

1. Description

This module adds F* support, powered by fstar-mode.el.

  • Syntax highlighting.
  • Interactively process F* files one definition at a time.
  • Query the running F* process to look up definitions, documentation, and theorems.

1.2. Module flags

This module has no flags.

1.4. Hacks

No hacks documented for this module.

2. Prerequisites

This module requires the latest release of F*. While fstar-mode supports the latest release of F*, you may have a better experience installing a more recent version from source. See F*’s INSTALL.md.

2.1. macOS

# ⎘
$ brew install fstar

2.2. Arch Linux

fstar is available in the AUR:

# ⎘
$ yay -S fstar

3. TODO Usage

This module has no usage documentation yet. Write some?

4. TODO Configuration

This module has no configuration documentation yet. Write some?

5. Troubleshooting

There are no known problems with this module. Report one?

If you’re having trouble getting F* to start correctly, you may need to configure a few variables in fstar-mode; see its README for more details.

6. TODO Appendix

This module has no appendix yet. Write one?