[[./img/fstar.png]]
Table of Contents :TOC_4_gh:noexport:
[[#description][Description]]
[[#install][Install]]
[[#key-bindings][Key bindings]]
Description This layer is just a wrapper around [[https://github.com/FStarLang/fstar-mode.el][fstar-mode]].
Install This layer is not integrated in the main spacemacs layer repository and probably won't be integrated since it is just a superficial wrapper. To use it you should rename the =fstar-layer= directory to =fstar=, place it in =~/.emacs.d/private/=, and add it to your =~/.spacemacs=. You will need to add =fstar= to the existing =dotspacemacs-configuration-layers= list in this file.
Key bindings
| Key Binding | Description | |-------------+----------------------------------------------| | ~SPC m n~ | eval next chunk of code | | ~SPC m u~ | retract last chunk of code | | ~SPC m i~ | eval/retract to point | | ~SPC m l~ | eval/retract to point in lax mode | | ~SPC m x~ | kill background z3 process (stop evaluation) | | ~SPC m b~ | eval the buffer in lax mode | | ~SPC m r~ | reload and eval the buffer to the point | | ~SPC m k~ | kill the underlying z3 process | |-------------+----------------------------------------------| | | Moving around | |-------------+----------------------------------------------| | ~SPC m .~ | jump to definition | | ~SPC m '~ | jump to related error | | ~SPC m j j~ | jump to definition | | ~SPC m j f~ | jump to definition in other frame | | ~SPC m j w~ | jump to definition in other window | | ~SPC m j e~ | jump to related error | | ~SPC m j F~ | jump to related error in other frame | | ~SPC m j W~ | jump to related error in other window | | ~SPC m j d~ | visit dependency | | ~SPC m j a~ | toggle between interface and implementation | |-------------+----------------------------------------------| | | Help !!! | |-------------+----------------------------------------------| | ~SPC m h y~ | yank help data at point | | ~SPC m h w~ | browse fstar wiki | | ~SPC m h W~ | browse fstar wiki in browser | | ~SPC m h o~ | list fstar options | | ~SPC m h p~ | toggle showing type at point | |-------------+----------------------------------------------| | | Others | |-------------+----------------------------------------------| | ~SPC m c~ | insert match | | ~SPC m e~ | evaluates expression | | ~SPC m E~ | evaluates expression with custom reduction | | ~SPC m s~ | search | | ~SPC m d~ | show documentation | | ~SPC m p~ | print the fstar term | | ~SPC m q~ | quit all satellite fstar windows | | ~SPC m P~ | print an outline of the current file |