Skip to content

Config

type Config =
    {
        FalsifiedSuffix: string option
        CheckMarker: string option
        CaptureImports: string array
        CollapseCodeOver: int option
    }
Assembly Nacara.Plugin.Rocq

Project settings read from navigator.json. All fields are optional in the file.

Fields

FalsifiedSuffix: string option

The name suffix marking a theorem that disproves a claim.

CheckMarker: string option

The text marking a comment as a record of property checking.

CaptureImports: string array

The modules imported before capture, which select the notations Rocq prints.

CollapseCodeOver: int option

The most lines a code body shows on load. A longer body starts closed, showing its first line.

Functions and values

none: Config

The configuration with every setting absent.

read (path: string) : Result<Config,string>

Reads the file at path. Returns Error naming the path when it is missing or malformed. An empty text setting is absent.